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.611    by (import prob_uniform UNIF_DEF_MONAD)
   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"