src/HOL/Import/HOL/HOL4Prob.thy
 changeset 17652 b1ef33ebfa17 parent 17644 bd59bfd4bf37 child 17694 b7870c2bd7df
```     1.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy	Mon Sep 26 15:56:28 2005 +0200
1.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Mon Sep 26 16:10:19 2005 +0200
1.3 @@ -9,14 +9,11 @@
1.4     f = (%b::bool. True) | f = (%b::bool. b) | f = Not"
1.5    by (import prob_extra BOOL_BOOL_CASES_THM)
1.6
1.7 -lemma EVEN_ODD_BASIC: "EVEN (0::nat) &
1.8 -~ EVEN (1::nat) &
1.9 -EVEN (2::nat) & ~ ODD (0::nat) & ODD (1::nat) & ~ ODD (2::nat)"
1.10 +lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
1.11    by (import prob_extra EVEN_ODD_BASIC)
1.12
1.13  lemma EVEN_ODD_EXISTS_EQ: "ALL n::nat.
1.14 -   EVEN n = (EX m::nat. n = (2::nat) * m) &
1.15 -   ODD n = (EX m::nat. n = Suc ((2::nat) * m))"
1.16 +   EVEN n = (EX m::nat. n = 2 * m) & ODD n = (EX m::nat. n = Suc (2 * m))"
1.17    by (import prob_extra EVEN_ODD_EXISTS_EQ)
1.18
1.19  lemma DIV_THEN_MULT: "ALL (p::nat) q::nat. Suc q * (p div Suc q) <= p"
1.20 @@ -60,20 +57,42 @@
1.21                            (bit.B0::bit)))))))))"
1.22    by (import prob_extra DIV_TWO_UNIQUE)
1.23
1.24 -lemma DIVISION_TWO: "ALL n::nat.
1.25 -   n = (2::nat) * (n div (2::nat)) + n mod (2::nat) &
1.26 -   (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))"
1.27 +lemma DIVISION_TWO: "ALL n::nat. n = 2 * (n div 2) + n mod 2 & (n mod 2 = 0 | n mod 2 = 1)"
1.28    by (import prob_extra DIVISION_TWO)
1.29
1.30 -lemma DIV_TWO: "ALL n::nat. n = (2::nat) * (n div (2::nat)) + n mod (2::nat)"
1.31 +lemma DIV_TWO: "ALL n::nat. n = 2 * (n div 2) + n mod 2"
1.32    by (import prob_extra DIV_TWO)
1.33
1.34 -lemma MOD_TWO: "(ALL (n::nat).
1.35 -    ((n mod (2::nat)) = (if (EVEN n) then (0::nat) else (1::nat))))"
1.36 +lemma MOD_TWO: "ALL n::nat. n mod 2 = (if EVEN n then 0 else 1)"
1.37    by (import prob_extra MOD_TWO)
1.38
1.39 -lemma DIV_TWO_BASIC: "(0::nat) div (2::nat) = (0::nat) &
1.40 -(1::nat) div (2::nat) = (0::nat) & (2::nat) div (2::nat) = (1::nat)"
1.41 +lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
1.42 + ((op =::nat => nat => bool)
1.43 +   ((op div::nat => nat => nat) (0::nat)
1.44 +     ((number_of::bin => nat)
1.45 +       ((op BIT::bin => bit => bin)
1.46 +         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.47 +         (bit.B0::bit))))
1.48 +   (0::nat))
1.49 + ((op &::bool => bool => bool)
1.50 +   ((op =::nat => nat => bool)
1.51 +     ((op div::nat => nat => nat) (1::nat)
1.52 +       ((number_of::bin => nat)
1.53 +         ((op BIT::bin => bit => bin)
1.54 +           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.55 +           (bit.B0::bit))))
1.56 +     (0::nat))
1.57 +   ((op =::nat => nat => bool)
1.58 +     ((op div::nat => nat => nat)
1.59 +       ((number_of::bin => nat)
1.60 +         ((op BIT::bin => bit => bin)
1.61 +           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.62 +           (bit.B0::bit)))
1.63 +       ((number_of::bin => nat)
1.64 +         ((op BIT::bin => bit => bin)
1.65 +           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.66 +           (bit.B0::bit))))
1.67 +     (1::nat)))"
1.68    by (import prob_extra DIV_TWO_BASIC)
1.69
1.70  lemma DIV_TWO_MONO: "(All::(nat => bool) => bool)
1.71 @@ -119,18 +138,35 @@
1.72               ((op <::nat => nat => bool) m n))))"
1.73    by (import prob_extra DIV_TWO_MONO_EVEN)
1.74
1.75 -lemma DIV_TWO_CANCEL: "ALL n::nat.
1.76 -   (2::nat) * n div (2::nat) = n & Suc ((2::nat) * n) div (2::nat) = n"
1.77 +lemma DIV_TWO_CANCEL: "ALL n::nat. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
1.78    by (import prob_extra DIV_TWO_CANCEL)
1.79
1.80 -lemma EXP_DIV_TWO: "ALL n::nat. (2::nat) ^ Suc n div (2::nat) = (2::nat) ^ n"
1.81 +lemma EXP_DIV_TWO: "(All::(nat => bool) => bool)
1.82 + (%n::nat.
1.83 +     (op =::nat => nat => bool)
1.84 +      ((op div::nat => nat => nat)
1.85 +        ((op ^::nat => nat => nat)
1.86 +          ((number_of::bin => nat)
1.87 +            ((op BIT::bin => bit => bin)
1.88 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.89 +              (bit.B0::bit)))
1.90 +          ((Suc::nat => nat) n))
1.91 +        ((number_of::bin => nat)
1.92 +          ((op BIT::bin => bit => bin)
1.93 +            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.94 +            (bit.B0::bit))))
1.95 +      ((op ^::nat => nat => nat)
1.96 +        ((number_of::bin => nat)
1.97 +          ((op BIT::bin => bit => bin)
1.98 +            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.99 +            (bit.B0::bit)))
1.100 +        n))"
1.101    by (import prob_extra EXP_DIV_TWO)
1.102
1.103 -lemma EVEN_EXP_TWO: "ALL n::nat. EVEN ((2::nat) ^ n) = (n ~= (0::nat))"
1.104 +lemma EVEN_EXP_TWO: "ALL n::nat. EVEN (2 ^ n) = (n ~= 0)"
1.105    by (import prob_extra EVEN_EXP_TWO)
1.106
1.107 -lemma DIV_TWO_EXP: "ALL (n::nat) k::nat.
1.108 -   (k div (2::nat) < (2::nat) ^ n) = (k < (2::nat) ^ Suc n)"
1.109 +lemma DIV_TWO_EXP: "ALL (n::nat) k::nat. (k div 2 < 2 ^ n) = (k < 2 ^ Suc n)"
1.110    by (import prob_extra DIV_TWO_EXP)
1.111
1.112  consts
1.113 @@ -195,13 +231,38 @@
1.114               z)))"
1.115    by (import prob_extra REAL_INF_MIN)
1.116
1.117 -lemma HALF_POS: "(0::real) < (1::real) / (2::real)"
1.118 +lemma HALF_POS: "(op <::real => real => bool) (0::real)
1.119 + ((op /::real => real => real) (1::real)
1.120 +   ((number_of::bin => real)
1.121 +     ((op BIT::bin => bit => bin)
1.122 +       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.123 +       (bit.B0::bit))))"
1.124    by (import prob_extra HALF_POS)
1.125
1.126 -lemma HALF_CANCEL: "(2::real) * ((1::real) / (2::real)) = (1::real)"
1.127 +lemma HALF_CANCEL: "(op =::real => real => bool)
1.128 + ((op *::real => real => real)
1.129 +   ((number_of::bin => real)
1.130 +     ((op BIT::bin => bit => bin)
1.131 +       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.132 +       (bit.B0::bit)))
1.133 +   ((op /::real => real => real) (1::real)
1.134 +     ((number_of::bin => real)
1.135 +       ((op BIT::bin => bit => bin)
1.136 +         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.137 +         (bit.B0::bit)))))
1.138 + (1::real)"
1.139    by (import prob_extra HALF_CANCEL)
1.140
1.141 -lemma POW_HALF_POS: "ALL n::nat. (0::real) < ((1::real) / (2::real)) ^ n"
1.142 +lemma POW_HALF_POS: "(All::(nat => bool) => bool)
1.143 + (%n::nat.
1.144 +     (op <::real => real => bool) (0::real)
1.145 +      ((op ^::real => nat => real)
1.146 +        ((op /::real => real => real) (1::real)
1.147 +          ((number_of::bin => real)
1.148 +            ((op BIT::bin => bit => bin)
1.149 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.150 +              (bit.B0::bit))))
1.151 +        n))"
1.152    by (import prob_extra POW_HALF_POS)
1.153
1.154  lemma POW_HALF_MONO: "(All::(nat => bool) => bool)
1.155 @@ -228,11 +289,32 @@
1.156                 m))))"
1.157    by (import prob_extra POW_HALF_MONO)
1.158
1.159 -lemma POW_HALF_TWICE: "ALL n::nat.
1.160 -   ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n"
1.161 +lemma POW_HALF_TWICE: "(All::(nat => bool) => bool)
1.162 + (%n::nat.
1.163 +     (op =::real => real => bool)
1.164 +      ((op ^::real => nat => real)
1.165 +        ((op /::real => real => real) (1::real)
1.166 +          ((number_of::bin => real)
1.167 +            ((op BIT::bin => bit => bin)
1.168 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.169 +              (bit.B0::bit))))
1.170 +        n)
1.171 +      ((op *::real => real => real)
1.172 +        ((number_of::bin => real)
1.173 +          ((op BIT::bin => bit => bin)
1.174 +            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.175 +            (bit.B0::bit)))
1.176 +        ((op ^::real => nat => real)
1.177 +          ((op /::real => real => real) (1::real)
1.178 +            ((number_of::bin => real)
1.179 +              ((op BIT::bin => bit => bin)
1.180 +                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.181 +                  (bit.B1::bit))
1.182 +                (bit.B0::bit))))
1.183 +          ((Suc::nat => nat) n))))"
1.184    by (import prob_extra POW_HALF_TWICE)
1.185
1.186 -lemma X_HALF_HALF: "ALL x::real. (1::real) / (2::real) * x + (1::real) / (2::real) * x = x"
1.187 +lemma X_HALF_HALF: "ALL x::real. 1 / 2 * x + 1 / 2 * x = x"
1.188    by (import prob_extra X_HALF_HALF)
1.189
1.190  lemma REAL_SUP_LE_X: "(All::((real => bool) => bool) => bool)
1.191 @@ -271,27 +353,60 @@
1.192    by (import prob_extra REAL_X_LE_SUP)
1.193
1.194  lemma ABS_BETWEEN_LE: "ALL (x::real) (y::real) d::real.
1.195 -   ((0::real) <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
1.196 +   (0 <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
1.197    by (import prob_extra ABS_BETWEEN_LE)
1.198
1.199 -lemma ONE_MINUS_HALF: "(1::real) - (1::real) / (2::real) = (1::real) / (2::real)"
1.200 +lemma ONE_MINUS_HALF: "(op =::real => real => bool)
1.201 + ((op -::real => real => real) (1::real)
1.202 +   ((op /::real => real => real) (1::real)
1.203 +     ((number_of::bin => real)
1.204 +       ((op BIT::bin => bit => bin)
1.205 +         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.206 +         (bit.B0::bit)))))
1.207 + ((op /::real => real => real) (1::real)
1.208 +   ((number_of::bin => real)
1.209 +     ((op BIT::bin => bit => bin)
1.210 +       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.211 +       (bit.B0::bit))))"
1.212    by (import prob_extra ONE_MINUS_HALF)
1.213
1.214 -lemma HALF_LT_1: "(1::real) / (2::real) < (1::real)"
1.215 +lemma HALF_LT_1: "(op <::real => real => bool)
1.216 + ((op /::real => real => real) (1::real)
1.217 +   ((number_of::bin => real)
1.218 +     ((op BIT::bin => bit => bin)
1.219 +       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.220 +       (bit.B0::bit))))
1.221 + (1::real)"
1.222    by (import prob_extra HALF_LT_1)
1.223
1.224 -lemma POW_HALF_EXP: "ALL n::nat. ((1::real) / (2::real)) ^ n = inverse (real ((2::nat) ^ n))"
1.225 +lemma POW_HALF_EXP: "(All::(nat => bool) => bool)
1.226 + (%n::nat.
1.227 +     (op =::real => real => bool)
1.228 +      ((op ^::real => nat => real)
1.229 +        ((op /::real => real => real) (1::real)
1.230 +          ((number_of::bin => real)
1.231 +            ((op BIT::bin => bit => bin)
1.232 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.233 +              (bit.B0::bit))))
1.234 +        n)
1.235 +      ((inverse::real => real)
1.236 +        ((real::nat => real)
1.237 +          ((op ^::nat => nat => nat)
1.238 +            ((number_of::bin => nat)
1.239 +              ((op BIT::bin => bit => bin)
1.240 +                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.241 +                  (bit.B1::bit))
1.242 +                (bit.B0::bit)))
1.243 +            n))))"
1.244    by (import prob_extra POW_HALF_EXP)
1.245
1.246 -lemma INV_SUC_POS: "ALL n::nat. (0::real) < (1::real) / real (Suc n)"
1.247 +lemma INV_SUC_POS: "ALL n::nat. 0 < 1 / real (Suc n)"
1.248    by (import prob_extra INV_SUC_POS)
1.249
1.250 -lemma INV_SUC_MAX: "ALL x::nat. (1::real) / real (Suc x) <= (1::real)"
1.251 +lemma INV_SUC_MAX: "ALL x::nat. 1 / real (Suc x) <= 1"
1.252    by (import prob_extra INV_SUC_MAX)
1.253
1.254 -lemma INV_SUC: "ALL n::nat.
1.255 -   (0::real) < (1::real) / real (Suc n) &
1.256 -   (1::real) / real (Suc n) <= (1::real)"
1.257 +lemma INV_SUC: "ALL n::nat. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
1.258    by (import prob_extra INV_SUC)
1.259
1.260  lemma ABS_UNIT_INTERVAL: "(All::(real => bool) => bool)
1.261 @@ -894,12 +1009,10 @@
1.262
1.263  defs
1.264    alg_longest_primdef: "alg_longest ==
1.265 -FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t)
1.266 - (0::nat)"
1.267 +FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t) 0"
1.268
1.269  lemma alg_longest_def: "alg_longest =
1.270 -FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t)
1.271 - (0::nat)"
1.272 +FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t) 0"
1.273    by (import prob_canon alg_longest_def)
1.274
1.275  consts
1.276 @@ -1948,9 +2061,9 @@
1.277    SHD :: "(nat => bool) => bool"
1.278
1.279  defs
1.280 -  SHD_primdef: "SHD == %f::nat => bool. f (0::nat)"
1.281 -
1.282 -lemma SHD_def: "ALL f::nat => bool. SHD f = f (0::nat)"
1.283 +  SHD_primdef: "SHD == %f::nat => bool. f 0"
1.284 +
1.285 +lemma SHD_def: "ALL f::nat => bool. SHD f = f 0"
1.286    by (import boolean_sequence SHD_def)
1.287
1.288  consts
1.289 @@ -1965,7 +2078,7 @@
1.290  consts
1.291    SCONS :: "bool => (nat => bool) => nat => bool"
1.292
1.293 -specification (SCONS_primdef: SCONS) SCONS_def: "(ALL (h::bool) t::nat => bool. SCONS h t (0::nat) = h) &
1.294 +specification (SCONS_primdef: SCONS) SCONS_def: "(ALL (h::bool) t::nat => bool. SCONS h t 0 = h) &
1.295  (ALL (h::bool) (t::nat => bool) n::nat. SCONS h t (Suc n) = t n)"
1.296    by (import boolean_sequence SCONS_def)
1.297
1.298 @@ -1990,14 +2103,14 @@
1.299  consts
1.300    STAKE :: "nat => (nat => bool) => bool list"
1.301
1.302 -specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s::nat => bool. STAKE (0::nat) s = []) &
1.303 +specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s::nat => bool. STAKE 0 s = []) &
1.304  (ALL (n::nat) s::nat => bool. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
1.305    by (import boolean_sequence STAKE_def)
1.306
1.307  consts
1.308    SDROP :: "nat => (nat => bool) => nat => bool"
1.309
1.310 -specification (SDROP_primdef: SDROP) SDROP_def: "SDROP (0::nat) = I & (ALL n::nat. SDROP (Suc n) = SDROP n o STL)"
1.311 +specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n::nat. SDROP (Suc n) = SDROP n o STL)"
1.312    by (import boolean_sequence SDROP_def)
1.313
1.314  lemma SCONS_SURJ: "ALL x::nat => bool. EX (xa::bool) t::nat => bool. x = SCONS xa t"
1.315 @@ -2271,10 +2384,9 @@
1.316  consts
1.317    alg_measure :: "bool list list => real"
1.318
1.319 -specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = (0::real) &
1.320 +specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
1.321  (ALL (l::bool list) rest::bool list list.
1.322 -    alg_measure (l # rest) =
1.323 -    ((1::real) / (2::real)) ^ length l + alg_measure rest)"
1.324 +    alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
1.325    by (import prob alg_measure_def)
1.326
1.327  consts
1.328 @@ -2311,18 +2423,42 @@
1.329                algebra_measure b = r & SUBSET (algebra_embed b) s)"
1.330    by (import prob prob_def)
1.331
1.332 -lemma ALG_TWINS_MEASURE: "ALL l::bool list.
1.333 -   ((1::real) / (2::real)) ^ length (SNOC True l) +
1.334 -   ((1::real) / (2::real)) ^ length (SNOC False l) =
1.335 -   ((1::real) / (2::real)) ^ length l"
1.336 +lemma ALG_TWINS_MEASURE: "(All::(bool list => bool) => bool)
1.337 + (%l::bool list.
1.338 +     (op =::real => real => bool)
1.339 +      ((op +::real => real => real)
1.340 +        ((op ^::real => nat => real)
1.341 +          ((op /::real => real => real) (1::real)
1.342 +            ((number_of::bin => real)
1.343 +              ((op BIT::bin => bit => bin)
1.344 +                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.345 +                  (bit.B1::bit))
1.346 +                (bit.B0::bit))))
1.347 +          ((size::bool list => nat)
1.348 +            ((SNOC::bool => bool list => bool list) (True::bool) l)))
1.349 +        ((op ^::real => nat => real)
1.350 +          ((op /::real => real => real) (1::real)
1.351 +            ((number_of::bin => real)
1.352 +              ((op BIT::bin => bit => bin)
1.353 +                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.354 +                  (bit.B1::bit))
1.355 +                (bit.B0::bit))))
1.356 +          ((size::bool list => nat)
1.357 +            ((SNOC::bool => bool list => bool list) (False::bool) l))))
1.358 +      ((op ^::real => nat => real)
1.359 +        ((op /::real => real => real) (1::real)
1.360 +          ((number_of::bin => real)
1.361 +            ((op BIT::bin => bit => bin)
1.362 +              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
1.363 +              (bit.B0::bit))))
1.364 +        ((size::bool list => nat) l)))"
1.365    by (import prob ALG_TWINS_MEASURE)
1.366
1.367 -lemma ALG_MEASURE_BASIC: "alg_measure [] = (0::real) &
1.368 -alg_measure [[]] = (1::real) &
1.369 -(ALL b::bool. alg_measure [[b]] = (1::real) / (2::real))"
1.370 +lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
1.371 +alg_measure [[]] = 1 & (ALL b::bool. alg_measure [[b]] = 1 / 2)"
1.372    by (import prob ALG_MEASURE_BASIC)
1.373
1.374 -lemma ALG_MEASURE_POS: "ALL l::bool list list. (0::real) <= alg_measure l"
1.375 +lemma ALG_MEASURE_POS: "ALL l::bool list list. 0 <= alg_measure l"
1.376    by (import prob ALG_MEASURE_POS)
1.377
1.378  lemma ALG_MEASURE_APPEND: "ALL (l1::bool list list) l2::bool list list.
1.379 @@ -2330,7 +2466,7 @@
1.380    by (import prob ALG_MEASURE_APPEND)
1.381
1.382  lemma ALG_MEASURE_TLS: "ALL (l::bool list list) b::bool.
1.383 -   (2::real) * alg_measure (map (op # b) l) = alg_measure l"
1.384 +   2 * alg_measure (map (op # b) l) = alg_measure l"
1.385    by (import prob ALG_MEASURE_TLS)
1.386
1.387  lemma ALG_CANON_PREFS_MONO: "ALL (l::bool list) b::bool list list.
1.388 @@ -2357,9 +2493,8 @@
1.389  lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l::bool list list. algebra_measure l = alg_measure (alg_canon l)"
1.390    by (import prob ALGEBRA_MEASURE_DEF_ALT)
1.391
1.392 -lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = (0::real) &
1.393 -algebra_measure [[]] = (1::real) &
1.394 -(ALL b::bool. algebra_measure [[b]] = (1::real) / (2::real))"
1.395 +lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
1.396 +algebra_measure [[]] = 1 & (ALL b::bool. algebra_measure [[b]] = 1 / 2)"
1.397    by (import prob ALGEBRA_MEASURE_BASIC)
1.398
1.399  lemma ALGEBRA_CANON_MEASURE_MAX: "(All::(bool list list => bool) => bool)
1.400 @@ -2370,7 +2505,7 @@
1.401          ((alg_measure::bool list list => real) l) (1::real)))"
1.402    by (import prob ALGEBRA_CANON_MEASURE_MAX)
1.403
1.404 -lemma ALGEBRA_MEASURE_MAX: "ALL l::bool list list. algebra_measure l <= (1::real)"
1.405 +lemma ALGEBRA_MEASURE_MAX: "ALL l::bool list list. algebra_measure l <= 1"
1.406    by (import prob ALGEBRA_MEASURE_MAX)
1.407
1.408  lemma ALGEBRA_MEASURE_MONO_EMBED: "(All::(bool list list => bool) => bool)
1.409 @@ -2458,9 +2593,9 @@
1.410  lemma PROB_ALGEBRA: "ALL l::bool list list. prob (algebra_embed l) = algebra_measure l"
1.411    by (import prob PROB_ALGEBRA)
1.412
1.413 -lemma PROB_BASIC: "prob EMPTY = (0::real) &
1.414 -prob pred_set.UNIV = (1::real) &
1.415 -(ALL b::bool. prob (%s::nat => bool. SHD s = b) = (1::real) / (2::real))"
1.416 +lemma PROB_BASIC: "prob EMPTY = 0 &
1.417 +prob pred_set.UNIV = 1 &
1.418 +(ALL b::bool. prob (%s::nat => bool. SHD s = b) = 1 / 2)"
1.419    by (import prob PROB_BASIC)
1.420
1.421  lemma PROB_ADDITIVE: "(All::(((nat => bool) => bool) => bool) => bool)
1.422 @@ -2578,7 +2713,7 @@
1.423               ((prob::((nat => bool) => bool) => real) t))))"
1.424    by (import prob PROB_SUBSET_MONO)
1.425
1.426 -lemma PROB_ALG: "ALL x::bool list. prob (alg_embed x) = ((1::real) / (2::real)) ^ length x"
1.427 +lemma PROB_ALG: "ALL x::bool list. prob (alg_embed x) = (1 / 2) ^ length x"
1.428    by (import prob PROB_ALG)
1.429
1.430  lemma PROB_STL: "(All::(((nat => bool) => bool) => bool) => bool)
1.431 @@ -2662,26 +2797,25 @@
1.432                 ((prob::((nat => bool) => bool) => real) p)))))"
1.433    by (import prob PROB_INTER_SHD)
1.434
1.435 -lemma ALGEBRA_MEASURE_POS: "ALL l::bool list list. (0::real) <= algebra_measure l"
1.436 +lemma ALGEBRA_MEASURE_POS: "ALL l::bool list list. 0 <= algebra_measure l"
1.437    by (import prob ALGEBRA_MEASURE_POS)
1.438
1.439 -lemma ALGEBRA_MEASURE_RANGE: "ALL l::bool list list.
1.440 -   (0::real) <= algebra_measure l & algebra_measure l <= (1::real)"
1.441 +lemma ALGEBRA_MEASURE_RANGE: "ALL l::bool list list. 0 <= algebra_measure l & algebra_measure l <= 1"
1.442    by (import prob ALGEBRA_MEASURE_RANGE)
1.443
1.444 -lemma PROB_POS: "ALL p::(nat => bool) => bool. (0::real) <= prob p"
1.445 +lemma PROB_POS: "ALL p::(nat => bool) => bool. 0 <= prob p"
1.446    by (import prob PROB_POS)
1.447
1.448 -lemma PROB_MAX: "ALL p::(nat => bool) => bool. prob p <= (1::real)"
1.449 +lemma PROB_MAX: "ALL p::(nat => bool) => bool. prob p <= 1"
1.450    by (import prob PROB_MAX)
1.451
1.452 -lemma PROB_RANGE: "ALL p::(nat => bool) => bool. (0::real) <= prob p & prob p <= (1::real)"
1.453 +lemma PROB_RANGE: "ALL p::(nat => bool) => bool. 0 <= prob p & prob p <= 1"
1.454    by (import prob PROB_RANGE)
1.455
1.456  lemma ABS_PROB: "ALL p::(nat => bool) => bool. abs (prob p) = prob p"
1.457    by (import prob ABS_PROB)
1.458
1.459 -lemma PROB_SHD: "ALL b::bool. prob (%s::nat => bool. SHD s = b) = (1::real) / (2::real)"
1.460 +lemma PROB_SHD: "ALL b::bool. prob (%s::nat => bool. SHD s = b) = 1 / 2"
1.461    by (import prob PROB_SHD)
1.462
1.463  lemma PROB_COMPL_LE1: "(All::(((nat => bool) => bool) => bool) => bool)
1.464 @@ -2719,11 +2853,10 @@
1.465
1.466  defs
1.467    pseudo_linear_tl_primdef: "pseudo_linear_tl ==
1.468 -%(a::nat) (b::nat) (n::nat) x::nat.
1.469 -   (a * x + b) mod ((2::nat) * n + (1::nat))"
1.470 +%(a::nat) (b::nat) (n::nat) x::nat. (a * x + b) mod (2 * n + 1)"
1.471
1.472  lemma pseudo_linear_tl_def: "ALL (a::nat) (b::nat) (n::nat) x::nat.
1.473 -   pseudo_linear_tl a b n x = (a * x + b) mod ((2::nat) * n + (1::nat))"
1.474 +   pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
1.475    by (import prob_pseudo pseudo_linear_tl_def)
1.476
1.477  lemma PSEUDO_LINEAR1_EXECUTE: "EX x::nat => nat => bool.
1.478 @@ -2828,7 +2961,7 @@
1.479    by (import prob_indep alg_cover_def)
1.480
1.481  consts
1.482 -  indep :: "((nat => bool) => 'a::type * (nat => bool)) => bool"
1.483 +  indep :: "((nat => bool) => 'a * (nat => bool)) => bool"
1.484
1.485  defs
1.486    indep_primdef: "indep ==
1.487 @@ -3520,21 +3653,19 @@
1.488  defs
1.489    unif_bound_primdef: "unif_bound ==
1.490  WFREC
1.491 - (SOME R::nat => nat => bool.
1.492 -     WF R & (ALL v::nat. R (Suc v div (2::nat)) (Suc v)))
1.493 + (SOME R::nat => nat => bool. WF R & (ALL v::nat. R (Suc v div 2) (Suc v)))
1.494   (%unif_bound::nat => nat.
1.495 -     nat_case (0::nat) (%v1::nat. Suc (unif_bound (Suc v1 div (2::nat)))))"
1.496 +     nat_case 0 (%v1::nat. Suc (unif_bound (Suc v1 div 2))))"
1.497
1.498  lemma unif_bound_primitive_def: "unif_bound =
1.499  WFREC
1.500 - (SOME R::nat => nat => bool.
1.501 -     WF R & (ALL v::nat. R (Suc v div (2::nat)) (Suc v)))
1.502 + (SOME R::nat => nat => bool. WF R & (ALL v::nat. R (Suc v div 2) (Suc v)))
1.503   (%unif_bound::nat => nat.
1.504 -     nat_case (0::nat) (%v1::nat. Suc (unif_bound (Suc v1 div (2::nat)))))"
1.505 +     nat_case 0 (%v1::nat. Suc (unif_bound (Suc v1 div 2))))"
1.506    by (import prob_uniform unif_bound_primitive_def)
1.507
1.508 -lemma unif_bound_def: "unif_bound (0::nat) = (0::nat) &
1.509 -unif_bound (Suc (v::nat)) = Suc (unif_bound (Suc v div (2::nat)))"
1.510 +lemma unif_bound_def: "unif_bound 0 = 0 &
1.511 +unif_bound (Suc (v::nat)) = Suc (unif_bound (Suc v div 2))"
1.512    by (import prob_uniform unif_bound_def)
1.513
1.514  lemma unif_bound_ind: "(All::((nat => bool) => bool) => bool)
1.515 @@ -3559,30 +3690,24 @@
1.516    "unif_tupled ==
1.517  WFREC
1.518   (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
1.519 -     WF R &
1.520 -     (ALL (s::nat => bool) v2::nat. R (Suc v2 div (2::nat), s) (Suc v2, s)))
1.521 +     WF R & (ALL (s::nat => bool) v2::nat. R (Suc v2 div 2, s) (Suc v2, s)))
1.522   (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
1.523       v1::nat => bool).
1.524 -     case v of 0 => (0::nat, v1)
1.525 +     case v of 0 => (0, v1)
1.526       | Suc (v3::nat) =>
1.527 -         let (m::nat, s'::nat => bool) =
1.528 -               unif_tupled (Suc v3 div (2::nat), v1)
1.529 -         in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m,
1.530 -             STL s'))"
1.531 +         let (m::nat, s'::nat => bool) = unif_tupled (Suc v3 div 2, v1)
1.532 +         in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
1.533
1.534  lemma unif_tupled_primitive_def: "unif_tupled =
1.535  WFREC
1.536   (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
1.537 -     WF R &
1.538 -     (ALL (s::nat => bool) v2::nat. R (Suc v2 div (2::nat), s) (Suc v2, s)))
1.539 +     WF R & (ALL (s::nat => bool) v2::nat. R (Suc v2 div 2, s) (Suc v2, s)))
1.540   (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
1.541       v1::nat => bool).
1.542 -     case v of 0 => (0::nat, v1)
1.543 +     case v of 0 => (0, v1)
1.544       | Suc (v3::nat) =>
1.545 -         let (m::nat, s'::nat => bool) =
1.546 -               unif_tupled (Suc v3 div (2::nat), v1)
1.547 -         in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m,
1.548 -             STL s'))"
1.549 +         let (m::nat, s'::nat => bool) = unif_tupled (Suc v3 div 2, v1)
1.550 +         in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
1.551    by (import prob_uniform unif_tupled_primitive_def)
1.552
1.553  consts
1.554 @@ -3594,10 +3719,10 @@
1.555  lemma unif_curried_def: "ALL (x::nat) x1::nat => bool. unif x x1 = unif_tupled (x, x1)"
1.556    by (import prob_uniform unif_curried_def)
1.557
1.558 -lemma unif_def: "unif (0::nat) (s::nat => bool) = (0::nat, s) &
1.559 +lemma unif_def: "unif 0 (s::nat => bool) = (0, s) &
1.560  unif (Suc (v2::nat)) s =
1.561 -(let (m::nat, s'::nat => bool) = unif (Suc v2 div (2::nat)) s
1.562 - in (if SHD s' then (2::nat) * m + (1::nat) else (2::nat) * m, STL s'))"
1.563 +(let (m::nat, s'::nat => bool) = unif (Suc v2 div 2) s
1.564 + in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
1.565    by (import prob_uniform unif_def)
1.566
1.567  lemma unif_ind: "(All::((nat => (nat => bool) => bool) => bool) => bool)
1.568 @@ -3871,19 +3996,19 @@
1.569               (%xa::nat. (All::((nat => bool) => bool) => bool) (P x xa)))))"
1.570    by (import prob_uniform uniform_ind)
1.571
1.572 -lemma uniform_def: "uniform (0::nat) (Suc (n::nat)) (s::nat => bool) = (0::nat, s) &
1.573 +lemma uniform_def: "uniform 0 (Suc (n::nat)) (s::nat => bool) = (0, s) &
1.574  uniform (Suc (t::nat)) (Suc n) s =
1.575  (let (xa::nat, x::nat => bool) = unif n s
1.576   in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
1.577    by (import prob_uniform uniform_def)
1.578
1.579 -lemma SUC_DIV_TWO_ZERO: "ALL n::nat. (Suc n div (2::nat) = (0::nat)) = (n = (0::nat))"
1.580 +lemma SUC_DIV_TWO_ZERO: "ALL n::nat. (Suc n div 2 = 0) = (n = 0)"
1.581    by (import prob_uniform SUC_DIV_TWO_ZERO)
1.582
1.583 -lemma UNIF_BOUND_LOWER: "ALL n::nat. n < (2::nat) ^ unif_bound n"
1.584 +lemma UNIF_BOUND_LOWER: "ALL n::nat. n < 2 ^ unif_bound n"
1.585    by (import prob_uniform UNIF_BOUND_LOWER)
1.586
1.587 -lemma UNIF_BOUND_LOWER_SUC: "ALL n::nat. Suc n <= (2::nat) ^ unif_bound n"
1.588 +lemma UNIF_BOUND_LOWER_SUC: "ALL n::nat. Suc n <= 2 ^ unif_bound n"
1.589    by (import prob_uniform UNIF_BOUND_LOWER_SUC)
1.590
1.591  lemma UNIF_BOUND_UPPER: "(All::(nat => bool) => bool)
1.592 @@ -3905,20 +4030,18 @@
1.593            n)))"
1.594    by (import prob_uniform UNIF_BOUND_UPPER)
1.595
1.596 -lemma UNIF_BOUND_UPPER_SUC: "ALL n::nat. (2::nat) ^ unif_bound n <= Suc ((2::nat) * n)"
1.597 +lemma UNIF_BOUND_UPPER_SUC: "ALL n::nat. 2 ^ unif_bound n <= Suc (2 * n)"
1.598    by (import prob_uniform UNIF_BOUND_UPPER_SUC)
1.599
1.600 -lemma UNIF_DEF_MONAD: "unif (0::nat) = UNIT (0::nat) &
1.601 +lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
1.602  (ALL n::nat.
1.603      unif (Suc n) =
1.604 -    BIND (unif (Suc n div (2::nat)))
1.605 +    BIND (unif (Suc n div 2))
1.606       (%m::nat.
1.607 -         BIND SDEST
1.608 -          (%b::bool.
1.609 -              UNIT (if b then (2::nat) * m + (1::nat) else (2::nat) * m))))"
1.610 +         BIND SDEST (%b::bool. UNIT (if b then 2 * m + 1 else 2 * m))))"
1.612
1.613 -lemma UNIFORM_DEF_MONAD: "(ALL x::nat. uniform (0::nat) (Suc x) = UNIT (0::nat)) &
1.614 +lemma UNIFORM_DEF_MONAD: "(ALL x::nat. uniform 0 (Suc x) = UNIT 0) &
1.615  (ALL (x::nat) xa::nat.
1.616      uniform (Suc x) (Suc xa) =
1.617      BIND (unif xa)
1.618 @@ -3931,45 +4054,18 @@
1.619  lemma INDEP_UNIFORM: "ALL (t::nat) n::nat. indep (uniform t (Suc n))"
1.620    by (import prob_uniform INDEP_UNIFORM)
1.621
1.622 -lemma PROB_UNIF: "(All::(nat => bool) => bool)
1.623 - (%n::nat.
1.624 -     (All::(nat => bool) => bool)
1.625 -      (%k::nat.
1.626 -          (op =::real => real => bool)
1.627 -           ((prob::((nat => bool) => bool) => real)
1.628 -             (%s::nat => bool.
1.629 -                 (op =::nat => nat => bool)
1.630 -                  ((fst::nat * (nat => bool) => nat)
1.631 -                    ((unif::nat => (nat => bool) => nat * (nat => bool)) n
1.632 -                      s))
1.633 -                  k))
1.634 -           ((If::bool => real => real => real)
1.635 -             ((op <::nat => nat => bool) k
1.636 -               ((op ^::nat => nat => nat)
1.637 -                 ((number_of::bin => nat)
1.638 -                   ((op BIT::bin => bit => bin)
1.639 -                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.640 -                       (bit.B1::bit))
1.641 -                     (bit.B0::bit)))
1.642 -                 ((unif_bound::nat => nat) n)))
1.643 -             ((op ^::real => nat => real)
1.644 -               ((op /::real => real => real) (1::real)
1.645 -                 ((number_of::bin => real)
1.646 -                   ((op BIT::bin => bit => bin)
1.647 -                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
1.648 -                       (bit.B1::bit))
1.649 -                     (bit.B0::bit))))
1.650 -               ((unif_bound::nat => nat) n))
1.651 -             (0::real))))"
1.652 +lemma PROB_UNIF: "ALL (n::nat) k::nat.
1.653 +   prob (%s::nat => bool. fst (unif n s) = k) =
1.654 +   (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
1.655    by (import prob_uniform PROB_UNIF)
1.656
1.657 -lemma UNIF_RANGE: "ALL (n::nat) s::nat => bool. fst (unif n s) < (2::nat) ^ unif_bound n"
1.658 +lemma UNIF_RANGE: "ALL (n::nat) s::nat => bool. fst (unif n s) < 2 ^ unif_bound n"
1.659    by (import prob_uniform UNIF_RANGE)
1.660
1.661  lemma PROB_UNIF_PAIR: "ALL (n::nat) (k::nat) k'::nat.
1.662     (prob (%s::nat => bool. fst (unif n s) = k) =
1.663      prob (%s::nat => bool. fst (unif n s) = k')) =
1.664 -   ((k < (2::nat) ^ unif_bound n) = (k' < (2::nat) ^ unif_bound n))"
1.665 +   ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
1.666    by (import prob_uniform PROB_UNIF_PAIR)
1.667
1.668  lemma PROB_UNIF_BOUND: "(All::(nat => bool) => bool)
1.669 @@ -4004,8 +4100,7 @@
1.670                   ((unif_bound::nat => nat) n))))))"
1.671    by (import prob_uniform PROB_UNIF_BOUND)
1.672
1.673 -lemma PROB_UNIF_GOOD: "ALL n::nat.
1.674 -   (1::real) / (2::real) <= prob (%s::nat => bool. fst (unif n s) < Suc n)"
1.675 +lemma PROB_UNIF_GOOD: "ALL n::nat. 1 / 2 <= prob (%s::nat => bool. fst (unif n s) < Suc n)"
1.676    by (import prob_uniform PROB_UNIF_GOOD)
1.677
1.678  lemma UNIFORM_RANGE: "ALL (t::nat) (n::nat) s::nat => bool. fst (uniform t (Suc n) s) < Suc n"
```