src/HOL/Import/HOL/HOL4Prob.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17694 b7870c2bd7df
child 20485 3078fd2eec7b
permissions -rw-r--r--
adaptions to codegen_package
     1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     2 
     3 theory HOL4Prob imports HOL4Real begin
     4 
     5 ;setup_theory prob_extra
     6 
     7 lemma BOOL_BOOL_CASES_THM: "ALL f::bool => bool.
     8    f = (%b::bool. False) |
     9    f = (%b::bool. True) | f = (%b::bool. b) | f = Not"
    10   by (import prob_extra BOOL_BOOL_CASES_THM)
    11 
    12 lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
    13   by (import prob_extra EVEN_ODD_BASIC)
    14 
    15 lemma EVEN_ODD_EXISTS_EQ: "ALL n::nat.
    16    EVEN n = (EX m::nat. n = 2 * m) & ODD n = (EX m::nat. n = Suc (2 * m))"
    17   by (import prob_extra EVEN_ODD_EXISTS_EQ)
    18 
    19 lemma DIV_THEN_MULT: "ALL (p::nat) q::nat. Suc q * (p div Suc q) <= p"
    20   by (import prob_extra DIV_THEN_MULT)
    21 
    22 lemma DIV_TWO_UNIQUE: "ALL (n::nat) (q::nat) r::nat.
    23    n = 2 * q + r & (r = 0 | r = 1) --> q = n div 2 & r = n mod 2"
    24   by (import prob_extra DIV_TWO_UNIQUE)
    25 
    26 lemma DIVISION_TWO: "ALL n::nat. n = 2 * (n div 2) + n mod 2 & (n mod 2 = 0 | n mod 2 = 1)"
    27   by (import prob_extra DIVISION_TWO)
    28 
    29 lemma DIV_TWO: "ALL n::nat. n = 2 * (n div 2) + n mod 2"
    30   by (import prob_extra DIV_TWO)
    31 
    32 lemma MOD_TWO: "ALL n::nat. n mod 2 = (if EVEN n then 0 else 1)"
    33   by (import prob_extra MOD_TWO)
    34 
    35 lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
    36  ((op =::nat => nat => bool)
    37    ((op div::nat => nat => nat) (0::nat)
    38      ((number_of::bin => nat)
    39        ((op BIT::bin => bit => bin)
    40          ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    41          (bit.B0::bit))))
    42    (0::nat))
    43  ((op &::bool => bool => bool)
    44    ((op =::nat => nat => bool)
    45      ((op div::nat => nat => nat) (1::nat)
    46        ((number_of::bin => nat)
    47          ((op BIT::bin => bit => bin)
    48            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    49            (bit.B0::bit))))
    50      (0::nat))
    51    ((op =::nat => nat => bool)
    52      ((op div::nat => nat => nat)
    53        ((number_of::bin => nat)
    54          ((op BIT::bin => bit => bin)
    55            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    56            (bit.B0::bit)))
    57        ((number_of::bin => nat)
    58          ((op BIT::bin => bit => bin)
    59            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    60            (bit.B0::bit))))
    61      (1::nat)))"
    62   by (import prob_extra DIV_TWO_BASIC)
    63 
    64 lemma DIV_TWO_MONO: "ALL (m::nat) n::nat. m div 2 < n div 2 --> m < n"
    65   by (import prob_extra DIV_TWO_MONO)
    66 
    67 lemma DIV_TWO_MONO_EVEN: "ALL (m::nat) n::nat. EVEN n --> (m div 2 < n div 2) = (m < n)"
    68   by (import prob_extra DIV_TWO_MONO_EVEN)
    69 
    70 lemma DIV_TWO_CANCEL: "ALL n::nat. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
    71   by (import prob_extra DIV_TWO_CANCEL)
    72 
    73 lemma EXP_DIV_TWO: "(All::(nat => bool) => bool)
    74  (%n::nat.
    75      (op =::nat => nat => bool)
    76       ((op div::nat => nat => nat)
    77         ((op ^::nat => nat => nat)
    78           ((number_of::bin => nat)
    79             ((op BIT::bin => bit => bin)
    80               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    81               (bit.B0::bit)))
    82           ((Suc::nat => nat) n))
    83         ((number_of::bin => nat)
    84           ((op BIT::bin => bit => bin)
    85             ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    86             (bit.B0::bit))))
    87       ((op ^::nat => nat => nat)
    88         ((number_of::bin => nat)
    89           ((op BIT::bin => bit => bin)
    90             ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    91             (bit.B0::bit)))
    92         n))"
    93   by (import prob_extra EXP_DIV_TWO)
    94 
    95 lemma EVEN_EXP_TWO: "ALL n::nat. EVEN (2 ^ n) = (n ~= 0)"
    96   by (import prob_extra EVEN_EXP_TWO)
    97 
    98 lemma DIV_TWO_EXP: "ALL (n::nat) k::nat. (k div 2 < 2 ^ n) = (k < 2 ^ Suc n)"
    99   by (import prob_extra DIV_TWO_EXP)
   100 
   101 consts
   102   inf :: "(real => bool) => real" 
   103 
   104 defs
   105   inf_primdef: "inf == %P::real => bool. - sup (IMAGE uminus P)"
   106 
   107 lemma inf_def: "ALL P::real => bool. inf P = - sup (IMAGE uminus P)"
   108   by (import prob_extra inf_def)
   109 
   110 lemma INF_DEF_ALT: "ALL P::real => bool. inf P = - sup (%r::real. P (- r))"
   111   by (import prob_extra INF_DEF_ALT)
   112 
   113 lemma REAL_SUP_EXISTS_UNIQUE: "ALL P::real => bool.
   114    Ex P & (EX z::real. ALL x::real. P x --> x <= z) -->
   115    (EX! s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
   116   by (import prob_extra REAL_SUP_EXISTS_UNIQUE)
   117 
   118 lemma REAL_SUP_MAX: "ALL (P::real => bool) z::real.
   119    P z & (ALL x::real. P x --> x <= z) --> sup P = z"
   120   by (import prob_extra REAL_SUP_MAX)
   121 
   122 lemma REAL_INF_MIN: "ALL (P::real => bool) z::real.
   123    P z & (ALL x::real. P x --> z <= x) --> inf P = z"
   124   by (import prob_extra REAL_INF_MIN)
   125 
   126 lemma HALF_POS: "(op <::real => real => bool) (0::real)
   127  ((op /::real => real => real) (1::real)
   128    ((number_of::bin => real)
   129      ((op BIT::bin => bit => bin)
   130        ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   131        (bit.B0::bit))))"
   132   by (import prob_extra HALF_POS)
   133 
   134 lemma HALF_CANCEL: "(op =::real => real => bool)
   135  ((op *::real => real => real)
   136    ((number_of::bin => real)
   137      ((op BIT::bin => bit => bin)
   138        ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   139        (bit.B0::bit)))
   140    ((op /::real => real => real) (1::real)
   141      ((number_of::bin => real)
   142        ((op BIT::bin => bit => bin)
   143          ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   144          (bit.B0::bit)))))
   145  (1::real)"
   146   by (import prob_extra HALF_CANCEL)
   147 
   148 lemma POW_HALF_POS: "(All::(nat => bool) => bool)
   149  (%n::nat.
   150      (op <::real => real => bool) (0::real)
   151       ((op ^::real => nat => real)
   152         ((op /::real => real => real) (1::real)
   153           ((number_of::bin => real)
   154             ((op BIT::bin => bit => bin)
   155               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   156               (bit.B0::bit))))
   157         n))"
   158   by (import prob_extra POW_HALF_POS)
   159 
   160 lemma POW_HALF_MONO: "(All::(nat => bool) => bool)
   161  (%m::nat.
   162      (All::(nat => bool) => bool)
   163       (%n::nat.
   164           (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n)
   165            ((op <=::real => real => bool)
   166              ((op ^::real => nat => real)
   167                ((op /::real => real => real) (1::real)
   168                  ((number_of::bin => real)
   169                    ((op BIT::bin => bit => bin)
   170                      ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   171                        (bit.B1::bit))
   172                      (bit.B0::bit))))
   173                n)
   174              ((op ^::real => nat => real)
   175                ((op /::real => real => real) (1::real)
   176                  ((number_of::bin => real)
   177                    ((op BIT::bin => bit => bin)
   178                      ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   179                        (bit.B1::bit))
   180                      (bit.B0::bit))))
   181                m))))"
   182   by (import prob_extra POW_HALF_MONO)
   183 
   184 lemma POW_HALF_TWICE: "(All::(nat => bool) => bool)
   185  (%n::nat.
   186      (op =::real => real => bool)
   187       ((op ^::real => nat => real)
   188         ((op /::real => real => real) (1::real)
   189           ((number_of::bin => real)
   190             ((op BIT::bin => bit => bin)
   191               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   192               (bit.B0::bit))))
   193         n)
   194       ((op *::real => real => real)
   195         ((number_of::bin => real)
   196           ((op BIT::bin => bit => bin)
   197             ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   198             (bit.B0::bit)))
   199         ((op ^::real => nat => real)
   200           ((op /::real => real => real) (1::real)
   201             ((number_of::bin => real)
   202               ((op BIT::bin => bit => bin)
   203                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   204                   (bit.B1::bit))
   205                 (bit.B0::bit))))
   206           ((Suc::nat => nat) n))))"
   207   by (import prob_extra POW_HALF_TWICE)
   208 
   209 lemma X_HALF_HALF: "ALL x::real. 1 / 2 * x + 1 / 2 * x = x"
   210   by (import prob_extra X_HALF_HALF)
   211 
   212 lemma REAL_SUP_LE_X: "ALL (P::real => bool) x::real.
   213    Ex P & (ALL r::real. P r --> r <= x) --> sup P <= x"
   214   by (import prob_extra REAL_SUP_LE_X)
   215 
   216 lemma REAL_X_LE_SUP: "ALL (P::real => bool) x::real.
   217    Ex P &
   218    (EX z::real. ALL r::real. P r --> r <= z) &
   219    (EX r::real. P r & x <= r) -->
   220    x <= sup P"
   221   by (import prob_extra REAL_X_LE_SUP)
   222 
   223 lemma ABS_BETWEEN_LE: "ALL (x::real) (y::real) d::real.
   224    (0 <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
   225   by (import prob_extra ABS_BETWEEN_LE)
   226 
   227 lemma ONE_MINUS_HALF: "(op =::real => real => bool)
   228  ((op -::real => real => real) (1::real)
   229    ((op /::real => real => real) (1::real)
   230      ((number_of::bin => real)
   231        ((op BIT::bin => bit => bin)
   232          ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   233          (bit.B0::bit)))))
   234  ((op /::real => real => real) (1::real)
   235    ((number_of::bin => real)
   236      ((op BIT::bin => bit => bin)
   237        ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   238        (bit.B0::bit))))"
   239   by (import prob_extra ONE_MINUS_HALF)
   240 
   241 lemma HALF_LT_1: "(op <::real => real => bool)
   242  ((op /::real => real => real) (1::real)
   243    ((number_of::bin => real)
   244      ((op BIT::bin => bit => bin)
   245        ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   246        (bit.B0::bit))))
   247  (1::real)"
   248   by (import prob_extra HALF_LT_1)
   249 
   250 lemma POW_HALF_EXP: "(All::(nat => bool) => bool)
   251  (%n::nat.
   252      (op =::real => real => bool)
   253       ((op ^::real => nat => real)
   254         ((op /::real => real => real) (1::real)
   255           ((number_of::bin => real)
   256             ((op BIT::bin => bit => bin)
   257               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   258               (bit.B0::bit))))
   259         n)
   260       ((inverse::real => real)
   261         ((real::nat => real)
   262           ((op ^::nat => nat => nat)
   263             ((number_of::bin => nat)
   264               ((op BIT::bin => bit => bin)
   265                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   266                   (bit.B1::bit))
   267                 (bit.B0::bit)))
   268             n))))"
   269   by (import prob_extra POW_HALF_EXP)
   270 
   271 lemma INV_SUC_POS: "ALL n::nat. 0 < 1 / real (Suc n)"
   272   by (import prob_extra INV_SUC_POS)
   273 
   274 lemma INV_SUC_MAX: "ALL x::nat. 1 / real (Suc x) <= 1"
   275   by (import prob_extra INV_SUC_MAX)
   276 
   277 lemma INV_SUC: "ALL n::nat. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
   278   by (import prob_extra INV_SUC)
   279 
   280 lemma ABS_UNIT_INTERVAL: "ALL (x::real) y::real.
   281    0 <= x & x <= 1 & 0 <= y & y <= 1 --> abs (x - y) <= 1"
   282   by (import prob_extra ABS_UNIT_INTERVAL)
   283 
   284 lemma MEM_NIL: "ALL l::'a::type list. (ALL x::'a::type. ~ x mem l) = (l = [])"
   285   by (import prob_extra MEM_NIL)
   286 
   287 lemma MAP_MEM: "ALL (f::'a::type => 'b::type) (l::'a::type list) x::'b::type.
   288    x mem map f l = (EX y::'a::type. y mem l & x = f y)"
   289   by (import prob_extra MAP_MEM)
   290 
   291 lemma MEM_NIL_MAP_CONS: "ALL (x::'a::type) l::'a::type list list. ~ [] mem map (op # x) l"
   292   by (import prob_extra MEM_NIL_MAP_CONS)
   293 
   294 lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type:l. True] = l"
   295   by (import prob_extra FILTER_TRUE)
   296 
   297 lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type:l. False] = []"
   298   by (import prob_extra FILTER_FALSE)
   299 
   300 lemma FILTER_MEM: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list.
   301    x mem filter P l --> P x"
   302   by (import prob_extra FILTER_MEM)
   303 
   304 lemma MEM_FILTER: "ALL (P::'a::type => bool) (l::'a::type list) x::'a::type.
   305    x mem filter P l --> x mem l"
   306   by (import prob_extra MEM_FILTER)
   307 
   308 lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type:l. y ~= x] = l"
   309   by (import prob_extra FILTER_OUT_ELT)
   310 
   311 lemma IS_PREFIX_NIL: "ALL x::'a::type list. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
   312   by (import prob_extra IS_PREFIX_NIL)
   313 
   314 lemma IS_PREFIX_REFL: "ALL x::'a::type list. IS_PREFIX x x"
   315   by (import prob_extra IS_PREFIX_REFL)
   316 
   317 lemma IS_PREFIX_ANTISYM: "ALL (x::'a::type list) y::'a::type list.
   318    IS_PREFIX y x & IS_PREFIX x y --> x = y"
   319   by (import prob_extra IS_PREFIX_ANTISYM)
   320 
   321 lemma IS_PREFIX_TRANS: "ALL (x::'a::type list) (y::'a::type list) z::'a::type list.
   322    IS_PREFIX x y & IS_PREFIX y z --> IS_PREFIX x z"
   323   by (import prob_extra IS_PREFIX_TRANS)
   324 
   325 lemma IS_PREFIX_BUTLAST: "ALL (x::'a::type) y::'a::type list. IS_PREFIX (x # y) (butlast (x # y))"
   326   by (import prob_extra IS_PREFIX_BUTLAST)
   327 
   328 lemma IS_PREFIX_LENGTH: "ALL (x::'a::type list) y::'a::type list.
   329    IS_PREFIX y x --> length x <= length y"
   330   by (import prob_extra IS_PREFIX_LENGTH)
   331 
   332 lemma IS_PREFIX_LENGTH_ANTI: "ALL (x::'a::type list) y::'a::type list.
   333    IS_PREFIX y x & length x = length y --> x = y"
   334   by (import prob_extra IS_PREFIX_LENGTH_ANTI)
   335 
   336 lemma IS_PREFIX_SNOC: "ALL (x::'a::type) (y::'a::type list) z::'a::type list.
   337    IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
   338   by (import prob_extra IS_PREFIX_SNOC)
   339 
   340 lemma FOLDR_MAP: "ALL (f::'b::type => 'c::type => 'c::type) (e::'c::type)
   341    (g::'a::type => 'b::type) l::'a::type list.
   342    foldr f (map g l) e = foldr (%x::'a::type. f (g x)) l e"
   343   by (import prob_extra FOLDR_MAP)
   344 
   345 lemma LAST_MEM: "ALL (h::'a::type) t::'a::type list. last (h # t) mem h # t"
   346   by (import prob_extra LAST_MEM)
   347 
   348 lemma LAST_MAP_CONS: "ALL (b::bool) (h::bool list) t::bool list list.
   349    EX x::bool list. last (map (op # b) (h # t)) = b # x"
   350   by (import prob_extra LAST_MAP_CONS)
   351 
   352 lemma EXISTS_LONGEST: "ALL (x::'a::type list) y::'a::type list list.
   353    EX z::'a::type list.
   354       z mem x # y &
   355       (ALL w::'a::type list. w mem x # y --> length w <= length z)"
   356   by (import prob_extra EXISTS_LONGEST)
   357 
   358 lemma UNION_DEF_ALT: "ALL (s::'a::type => bool) t::'a::type => bool.
   359    pred_set.UNION s t = (%x::'a::type. s x | t x)"
   360   by (import prob_extra UNION_DEF_ALT)
   361 
   362 lemma INTER_UNION_RDISTRIB: "ALL (p::'a::type => bool) (q::'a::type => bool) r::'a::type => bool.
   363    pred_set.INTER (pred_set.UNION p q) r =
   364    pred_set.UNION (pred_set.INTER p r) (pred_set.INTER q r)"
   365   by (import prob_extra INTER_UNION_RDISTRIB)
   366 
   367 lemma SUBSET_EQ: "ALL (x::'a::type => bool) xa::'a::type => bool.
   368    (x = xa) = (SUBSET x xa & SUBSET xa x)"
   369   by (import prob_extra SUBSET_EQ)
   370 
   371 lemma INTER_IS_EMPTY: "ALL (s::'a::type => bool) t::'a::type => bool.
   372    (pred_set.INTER s t = EMPTY) = (ALL x::'a::type. ~ s x | ~ t x)"
   373   by (import prob_extra INTER_IS_EMPTY)
   374 
   375 lemma UNION_DISJOINT_SPLIT: "ALL (s::'a::type => bool) (t::'a::type => bool) u::'a::type => bool.
   376    pred_set.UNION s t = pred_set.UNION s u &
   377    pred_set.INTER s t = EMPTY & pred_set.INTER s u = EMPTY -->
   378    t = u"
   379   by (import prob_extra UNION_DISJOINT_SPLIT)
   380 
   381 lemma GSPEC_DEF_ALT: "ALL f::'a::type => 'b::type * bool.
   382    GSPEC f = (%v::'b::type. EX x::'a::type. (v, True) = f x)"
   383   by (import prob_extra GSPEC_DEF_ALT)
   384 
   385 ;end_setup
   386 
   387 ;setup_theory prob_canon
   388 
   389 consts
   390   alg_twin :: "bool list => bool list => bool" 
   391 
   392 defs
   393   alg_twin_primdef: "alg_twin ==
   394 %(x::bool list) y::bool list.
   395    EX l::bool list. x = SNOC True l & y = SNOC False l"
   396 
   397 lemma alg_twin_def: "ALL (x::bool list) y::bool list.
   398    alg_twin x y = (EX l::bool list. x = SNOC True l & y = SNOC False l)"
   399   by (import prob_canon alg_twin_def)
   400 
   401 constdefs
   402   alg_order_tupled :: "bool list * bool list => bool" 
   403   "(op ==::(bool list * bool list => bool)
   404         => (bool list * bool list => bool) => prop)
   405  (alg_order_tupled::bool list * bool list => bool)
   406  ((WFREC::(bool list * bool list => bool list * bool list => bool)
   407           => ((bool list * bool list => bool)
   408               => bool list * bool list => bool)
   409              => bool list * bool list => bool)
   410    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   411           => bool list * bool list => bool list * bool list => bool)
   412      (%R::bool list * bool list => bool list * bool list => bool.
   413          (op &::bool => bool => bool)
   414           ((WF::(bool list * bool list => bool list * bool list => bool)
   415                 => bool)
   416             R)
   417           ((All::(bool => bool) => bool)
   418             (%h'::bool.
   419                 (All::(bool => bool) => bool)
   420                  (%h::bool.
   421                      (All::(bool list => bool) => bool)
   422                       (%t'::bool list.
   423                           (All::(bool list => bool) => bool)
   424                            (%t::bool list.
   425                                R ((Pair::bool list
   426    => bool list => bool list * bool list)
   427                                    t t')
   428                                 ((Pair::bool list
   429   => bool list => bool list * bool list)
   430                                   ((op #::bool => bool list => bool list) h
   431                                     t)
   432                                   ((op #::bool => bool list => bool list) h'
   433                                     t')))))))))
   434    (%alg_order_tupled::bool list * bool list => bool.
   435        (split::(bool list => bool list => bool)
   436                => bool list * bool list => bool)
   437         (%(v::bool list) v1::bool list.
   438             (list_case::bool
   439                         => (bool => bool list => bool) => bool list => bool)
   440              ((list_case::bool
   441                           => (bool => bool list => bool)
   442                              => bool list => bool)
   443                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   444              (%(v4::bool) v5::bool list.
   445                  (list_case::bool
   446                              => (bool => bool list => bool)
   447                                 => bool list => bool)
   448                   (False::bool)
   449                   (%(v10::bool) v11::bool list.
   450                       (op |::bool => bool => bool)
   451                        ((op &::bool => bool => bool)
   452                          ((op =::bool => bool => bool) v4 (True::bool))
   453                          ((op =::bool => bool => bool) v10 (False::bool)))
   454                        ((op &::bool => bool => bool)
   455                          ((op =::bool => bool => bool) v4 v10)
   456                          (alg_order_tupled
   457                            ((Pair::bool list
   458                                    => bool list => bool list * bool list)
   459                              v5 v11))))
   460                   v1)
   461              v)))"
   462 
   463 lemma alg_order_tupled_primitive_def: "(op =::(bool list * bool list => bool)
   464        => (bool list * bool list => bool) => bool)
   465  (alg_order_tupled::bool list * bool list => bool)
   466  ((WFREC::(bool list * bool list => bool list * bool list => bool)
   467           => ((bool list * bool list => bool)
   468               => bool list * bool list => bool)
   469              => bool list * bool list => bool)
   470    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   471           => bool list * bool list => bool list * bool list => bool)
   472      (%R::bool list * bool list => bool list * bool list => bool.
   473          (op &::bool => bool => bool)
   474           ((WF::(bool list * bool list => bool list * bool list => bool)
   475                 => bool)
   476             R)
   477           ((All::(bool => bool) => bool)
   478             (%h'::bool.
   479                 (All::(bool => bool) => bool)
   480                  (%h::bool.
   481                      (All::(bool list => bool) => bool)
   482                       (%t'::bool list.
   483                           (All::(bool list => bool) => bool)
   484                            (%t::bool list.
   485                                R ((Pair::bool list
   486    => bool list => bool list * bool list)
   487                                    t t')
   488                                 ((Pair::bool list
   489   => bool list => bool list * bool list)
   490                                   ((op #::bool => bool list => bool list) h
   491                                     t)
   492                                   ((op #::bool => bool list => bool list) h'
   493                                     t')))))))))
   494    (%alg_order_tupled::bool list * bool list => bool.
   495        (split::(bool list => bool list => bool)
   496                => bool list * bool list => bool)
   497         (%(v::bool list) v1::bool list.
   498             (list_case::bool
   499                         => (bool => bool list => bool) => bool list => bool)
   500              ((list_case::bool
   501                           => (bool => bool list => bool)
   502                              => bool list => bool)
   503                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   504              (%(v4::bool) v5::bool list.
   505                  (list_case::bool
   506                              => (bool => bool list => bool)
   507                                 => bool list => bool)
   508                   (False::bool)
   509                   (%(v10::bool) v11::bool list.
   510                       (op |::bool => bool => bool)
   511                        ((op &::bool => bool => bool)
   512                          ((op =::bool => bool => bool) v4 (True::bool))
   513                          ((op =::bool => bool => bool) v10 (False::bool)))
   514                        ((op &::bool => bool => bool)
   515                          ((op =::bool => bool => bool) v4 v10)
   516                          (alg_order_tupled
   517                            ((Pair::bool list
   518                                    => bool list => bool list * bool list)
   519                              v5 v11))))
   520                   v1)
   521              v)))"
   522   by (import prob_canon alg_order_tupled_primitive_def)
   523 
   524 consts
   525   alg_order :: "bool list => bool list => bool" 
   526 
   527 defs
   528   alg_order_primdef: "alg_order == %(x::bool list) x1::bool list. alg_order_tupled (x, x1)"
   529 
   530 lemma alg_order_curried_def: "ALL (x::bool list) x1::bool list. alg_order x x1 = alg_order_tupled (x, x1)"
   531   by (import prob_canon alg_order_curried_def)
   532 
   533 lemma alg_order_ind: "ALL P::bool list => bool list => bool.
   534    (ALL (x::bool) xa::bool list. P [] (x # xa)) &
   535    P [] [] &
   536    (ALL (x::bool) xa::bool list. P (x # xa) []) &
   537    (ALL (x::bool) (xa::bool list) (xb::bool) xc::bool list.
   538        P xa xc --> P (x # xa) (xb # xc)) -->
   539    (ALL x::bool list. All (P x))"
   540   by (import prob_canon alg_order_ind)
   541 
   542 lemma alg_order_def: "alg_order [] ((v6::bool) # (v7::bool list)) = True &
   543 alg_order [] [] = True &
   544 alg_order ((v2::bool) # (v3::bool list)) [] = False &
   545 alg_order ((h::bool) # (t::bool list)) ((h'::bool) # (t'::bool list)) =
   546 (h = True & h' = False | h = h' & alg_order t t')"
   547   by (import prob_canon alg_order_def)
   548 
   549 consts
   550   alg_sorted :: "bool list list => bool" 
   551 
   552 defs
   553   alg_sorted_primdef: "alg_sorted ==
   554 WFREC
   555  (SOME R::bool list list => bool list list => bool.
   556      WF R &
   557      (ALL (x::bool list) (z::bool list list) y::bool list.
   558          R (y # z) (x # y # z)))
   559  (%alg_sorted::bool list list => bool.
   560      list_case True
   561       (%v2::bool list.
   562           list_case True
   563            (%(v6::bool list) v7::bool list list.
   564                alg_order v2 v6 & alg_sorted (v6 # v7))))"
   565 
   566 lemma alg_sorted_primitive_def: "alg_sorted =
   567 WFREC
   568  (SOME R::bool list list => bool list list => bool.
   569      WF R &
   570      (ALL (x::bool list) (z::bool list list) y::bool list.
   571          R (y # z) (x # y # z)))
   572  (%alg_sorted::bool list list => bool.
   573      list_case True
   574       (%v2::bool list.
   575           list_case True
   576            (%(v6::bool list) v7::bool list list.
   577                alg_order v2 v6 & alg_sorted (v6 # v7))))"
   578   by (import prob_canon alg_sorted_primitive_def)
   579 
   580 lemma alg_sorted_ind: "ALL P::bool list list => bool.
   581    (ALL (x::bool list) (y::bool list) z::bool list list.
   582        P (y # z) --> P (x # y # z)) &
   583    (ALL v::bool list. P [v]) & P [] -->
   584    All P"
   585   by (import prob_canon alg_sorted_ind)
   586 
   587 lemma alg_sorted_def: "alg_sorted ((x::bool list) # (y::bool list) # (z::bool list list)) =
   588 (alg_order x y & alg_sorted (y # z)) &
   589 alg_sorted [v::bool list] = True & alg_sorted [] = True"
   590   by (import prob_canon alg_sorted_def)
   591 
   592 consts
   593   alg_prefixfree :: "bool list list => bool" 
   594 
   595 defs
   596   alg_prefixfree_primdef: "alg_prefixfree ==
   597 WFREC
   598  (SOME R::bool list list => bool list list => bool.
   599      WF R &
   600      (ALL (x::bool list) (z::bool list list) y::bool list.
   601          R (y # z) (x # y # z)))
   602  (%alg_prefixfree::bool list list => bool.
   603      list_case True
   604       (%v2::bool list.
   605           list_case True
   606            (%(v6::bool list) v7::bool list list.
   607                ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   608 
   609 lemma alg_prefixfree_primitive_def: "alg_prefixfree =
   610 WFREC
   611  (SOME R::bool list list => bool list list => bool.
   612      WF R &
   613      (ALL (x::bool list) (z::bool list list) y::bool list.
   614          R (y # z) (x # y # z)))
   615  (%alg_prefixfree::bool list list => bool.
   616      list_case True
   617       (%v2::bool list.
   618           list_case True
   619            (%(v6::bool list) v7::bool list list.
   620                ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   621   by (import prob_canon alg_prefixfree_primitive_def)
   622 
   623 lemma alg_prefixfree_ind: "ALL P::bool list list => bool.
   624    (ALL (x::bool list) (y::bool list) z::bool list list.
   625        P (y # z) --> P (x # y # z)) &
   626    (ALL v::bool list. P [v]) & P [] -->
   627    All P"
   628   by (import prob_canon alg_prefixfree_ind)
   629 
   630 lemma alg_prefixfree_def: "alg_prefixfree ((x::bool list) # (y::bool list) # (z::bool list list)) =
   631 (~ IS_PREFIX y x & alg_prefixfree (y # z)) &
   632 alg_prefixfree [v::bool list] = True & alg_prefixfree [] = True"
   633   by (import prob_canon alg_prefixfree_def)
   634 
   635 consts
   636   alg_twinfree :: "bool list list => bool" 
   637 
   638 defs
   639   alg_twinfree_primdef: "alg_twinfree ==
   640 WFREC
   641  (SOME R::bool list list => bool list list => bool.
   642      WF R &
   643      (ALL (x::bool list) (z::bool list list) y::bool list.
   644          R (y # z) (x # y # z)))
   645  (%alg_twinfree::bool list list => bool.
   646      list_case True
   647       (%v2::bool list.
   648           list_case True
   649            (%(v6::bool list) v7::bool list list.
   650                ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   651 
   652 lemma alg_twinfree_primitive_def: "alg_twinfree =
   653 WFREC
   654  (SOME R::bool list list => bool list list => bool.
   655      WF R &
   656      (ALL (x::bool list) (z::bool list list) y::bool list.
   657          R (y # z) (x # y # z)))
   658  (%alg_twinfree::bool list list => bool.
   659      list_case True
   660       (%v2::bool list.
   661           list_case True
   662            (%(v6::bool list) v7::bool list list.
   663                ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   664   by (import prob_canon alg_twinfree_primitive_def)
   665 
   666 lemma alg_twinfree_ind: "ALL P::bool list list => bool.
   667    (ALL (x::bool list) (y::bool list) z::bool list list.
   668        P (y # z) --> P (x # y # z)) &
   669    (ALL v::bool list. P [v]) & P [] -->
   670    All P"
   671   by (import prob_canon alg_twinfree_ind)
   672 
   673 lemma alg_twinfree_def: "alg_twinfree ((x::bool list) # (y::bool list) # (z::bool list list)) =
   674 (~ alg_twin x y & alg_twinfree (y # z)) &
   675 alg_twinfree [v::bool list] = True & alg_twinfree [] = True"
   676   by (import prob_canon alg_twinfree_def)
   677 
   678 consts
   679   alg_longest :: "bool list list => nat" 
   680 
   681 defs
   682   alg_longest_primdef: "alg_longest ==
   683 FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t) 0"
   684 
   685 lemma alg_longest_def: "alg_longest =
   686 FOLDR (%(h::bool list) t::nat. if t <= length h then length h else t) 0"
   687   by (import prob_canon alg_longest_def)
   688 
   689 consts
   690   alg_canon_prefs :: "bool list => bool list list => bool list list" 
   691 
   692 specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l::bool list. alg_canon_prefs l [] = [l]) &
   693 (ALL (l::bool list) (h::bool list) t::bool list list.
   694     alg_canon_prefs l (h # t) =
   695     (if IS_PREFIX h l then alg_canon_prefs l t else l # h # t))"
   696   by (import prob_canon alg_canon_prefs_def)
   697 
   698 consts
   699   alg_canon_find :: "bool list => bool list list => bool list list" 
   700 
   701 specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l::bool list. alg_canon_find l [] = [l]) &
   702 (ALL (l::bool list) (h::bool list) t::bool list list.
   703     alg_canon_find l (h # t) =
   704     (if alg_order h l
   705      then if IS_PREFIX l h then h # t else h # alg_canon_find l t
   706      else alg_canon_prefs l (h # t)))"
   707   by (import prob_canon alg_canon_find_def)
   708 
   709 consts
   710   alg_canon1 :: "bool list list => bool list list" 
   711 
   712 defs
   713   alg_canon1_primdef: "alg_canon1 == FOLDR alg_canon_find []"
   714 
   715 lemma alg_canon1_def: "alg_canon1 = FOLDR alg_canon_find []"
   716   by (import prob_canon alg_canon1_def)
   717 
   718 consts
   719   alg_canon_merge :: "bool list => bool list list => bool list list" 
   720 
   721 specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l::bool list. alg_canon_merge l [] = [l]) &
   722 (ALL (l::bool list) (h::bool list) t::bool list list.
   723     alg_canon_merge l (h # t) =
   724     (if alg_twin l h then alg_canon_merge (butlast h) t else l # h # t))"
   725   by (import prob_canon alg_canon_merge_def)
   726 
   727 consts
   728   alg_canon2 :: "bool list list => bool list list" 
   729 
   730 defs
   731   alg_canon2_primdef: "alg_canon2 == FOLDR alg_canon_merge []"
   732 
   733 lemma alg_canon2_def: "alg_canon2 = FOLDR alg_canon_merge []"
   734   by (import prob_canon alg_canon2_def)
   735 
   736 consts
   737   alg_canon :: "bool list list => bool list list" 
   738 
   739 defs
   740   alg_canon_primdef: "alg_canon == %l::bool list list. alg_canon2 (alg_canon1 l)"
   741 
   742 lemma alg_canon_def: "ALL l::bool list list. alg_canon l = alg_canon2 (alg_canon1 l)"
   743   by (import prob_canon alg_canon_def)
   744 
   745 consts
   746   algebra_canon :: "bool list list => bool" 
   747 
   748 defs
   749   algebra_canon_primdef: "algebra_canon == %l::bool list list. alg_canon l = l"
   750 
   751 lemma algebra_canon_def: "ALL l::bool list list. algebra_canon l = (alg_canon l = l)"
   752   by (import prob_canon algebra_canon_def)
   753 
   754 lemma ALG_TWIN_NIL: "ALL l::bool list. ~ alg_twin l [] & ~ alg_twin [] l"
   755   by (import prob_canon ALG_TWIN_NIL)
   756 
   757 lemma ALG_TWIN_SING: "ALL (x::bool) l::bool list.
   758    alg_twin [x] l = (x = True & l = [False]) &
   759    alg_twin l [x] = (l = [True] & x = False)"
   760   by (import prob_canon ALG_TWIN_SING)
   761 
   762 lemma ALG_TWIN_CONS: "ALL (x::bool) (y::bool) (z::bool list) (h::bool) t::bool list.
   763    alg_twin (x # y # z) (h # t) = (x = h & alg_twin (y # z) t) &
   764    alg_twin (h # t) (x # y # z) = (x = h & alg_twin t (y # z))"
   765   by (import prob_canon ALG_TWIN_CONS)
   766 
   767 lemma ALG_TWIN_REDUCE: "ALL (h::bool) (t::bool list) t'::bool list.
   768    alg_twin (h # t) (h # t') = alg_twin t t'"
   769   by (import prob_canon ALG_TWIN_REDUCE)
   770 
   771 lemma ALG_TWINS_PREFIX: "ALL (x::bool list) l::bool list.
   772    IS_PREFIX x l -->
   773    x = l | IS_PREFIX x (SNOC True l) | IS_PREFIX x (SNOC False l)"
   774   by (import prob_canon ALG_TWINS_PREFIX)
   775 
   776 lemma ALG_ORDER_NIL: "ALL x::bool list. alg_order [] x & alg_order x [] = (x = [])"
   777   by (import prob_canon ALG_ORDER_NIL)
   778 
   779 lemma ALG_ORDER_REFL: "ALL x::bool list. alg_order x x"
   780   by (import prob_canon ALG_ORDER_REFL)
   781 
   782 lemma ALG_ORDER_ANTISYM: "ALL (x::bool list) y::bool list. alg_order x y & alg_order y x --> x = y"
   783   by (import prob_canon ALG_ORDER_ANTISYM)
   784 
   785 lemma ALG_ORDER_TRANS: "ALL (x::bool list) (y::bool list) z::bool list.
   786    alg_order x y & alg_order y z --> alg_order x z"
   787   by (import prob_canon ALG_ORDER_TRANS)
   788 
   789 lemma ALG_ORDER_TOTAL: "ALL (x::bool list) y::bool list. alg_order x y | alg_order y x"
   790   by (import prob_canon ALG_ORDER_TOTAL)
   791 
   792 lemma ALG_ORDER_PREFIX: "ALL (x::bool list) y::bool list. IS_PREFIX y x --> alg_order x y"
   793   by (import prob_canon ALG_ORDER_PREFIX)
   794 
   795 lemma ALG_ORDER_PREFIX_ANTI: "ALL (x::bool list) y::bool list. alg_order x y & IS_PREFIX x y --> x = y"
   796   by (import prob_canon ALG_ORDER_PREFIX_ANTI)
   797 
   798 lemma ALG_ORDER_PREFIX_MONO: "ALL (x::bool list) (y::bool list) z::bool list.
   799    alg_order x y & alg_order y z & IS_PREFIX z x --> IS_PREFIX y x"
   800   by (import prob_canon ALG_ORDER_PREFIX_MONO)
   801 
   802 lemma ALG_ORDER_PREFIX_TRANS: "ALL (x::bool list) (y::bool list) z::bool list.
   803    alg_order x y & IS_PREFIX y z --> alg_order x z | IS_PREFIX x z"
   804   by (import prob_canon ALG_ORDER_PREFIX_TRANS)
   805 
   806 lemma ALG_ORDER_SNOC: "ALL (x::bool) l::bool list. ~ alg_order (SNOC x l) l"
   807   by (import prob_canon ALG_ORDER_SNOC)
   808 
   809 lemma ALG_SORTED_MIN: "ALL (h::bool list) t::bool list list.
   810    alg_sorted (h # t) --> (ALL x::bool list. x mem t --> alg_order h x)"
   811   by (import prob_canon ALG_SORTED_MIN)
   812 
   813 lemma ALG_SORTED_DEF_ALT: "ALL (h::bool list) t::bool list list.
   814    alg_sorted (h # t) =
   815    ((ALL x::bool list. x mem t --> alg_order h x) & alg_sorted t)"
   816   by (import prob_canon ALG_SORTED_DEF_ALT)
   817 
   818 lemma ALG_SORTED_TL: "ALL (h::bool list) t::bool list list. alg_sorted (h # t) --> alg_sorted t"
   819   by (import prob_canon ALG_SORTED_TL)
   820 
   821 lemma ALG_SORTED_MONO: "ALL (x::bool list) (y::bool list) z::bool list list.
   822    alg_sorted (x # y # z) --> alg_sorted (x # z)"
   823   by (import prob_canon ALG_SORTED_MONO)
   824 
   825 lemma ALG_SORTED_TLS: "ALL (l::bool list list) b::bool. alg_sorted (map (op # b) l) = alg_sorted l"
   826   by (import prob_canon ALG_SORTED_TLS)
   827 
   828 lemma ALG_SORTED_STEP: "ALL (l1::bool list list) l2::bool list list.
   829    alg_sorted (map (op # True) l1 @ map (op # False) l2) =
   830    (alg_sorted l1 & alg_sorted l2)"
   831   by (import prob_canon ALG_SORTED_STEP)
   832 
   833 lemma ALG_SORTED_APPEND: "ALL (h::bool list) (h'::bool list) (t::bool list list) t'::bool list list.
   834    alg_sorted ((h # t) @ h' # t') =
   835    (alg_sorted (h # t) & alg_sorted (h' # t') & alg_order (last (h # t)) h')"
   836   by (import prob_canon ALG_SORTED_APPEND)
   837 
   838 lemma ALG_SORTED_FILTER: "ALL (P::bool list => bool) b::bool list list.
   839    alg_sorted b --> alg_sorted (filter P b)"
   840   by (import prob_canon ALG_SORTED_FILTER)
   841 
   842 lemma ALG_PREFIXFREE_TL: "ALL (h::bool list) t::bool list list.
   843    alg_prefixfree (h # t) --> alg_prefixfree t"
   844   by (import prob_canon ALG_PREFIXFREE_TL)
   845 
   846 lemma ALG_PREFIXFREE_MONO: "ALL (x::bool list) (y::bool list) z::bool list list.
   847    alg_sorted (x # y # z) & alg_prefixfree (x # y # z) -->
   848    alg_prefixfree (x # z)"
   849   by (import prob_canon ALG_PREFIXFREE_MONO)
   850 
   851 lemma ALG_PREFIXFREE_ELT: "ALL (h::bool list) t::bool list list.
   852    alg_sorted (h # t) & alg_prefixfree (h # t) -->
   853    (ALL x::bool list. x mem t --> ~ IS_PREFIX x h & ~ IS_PREFIX h x)"
   854   by (import prob_canon ALG_PREFIXFREE_ELT)
   855 
   856 lemma ALG_PREFIXFREE_TLS: "ALL (l::bool list list) b::bool.
   857    alg_prefixfree (map (op # b) l) = alg_prefixfree l"
   858   by (import prob_canon ALG_PREFIXFREE_TLS)
   859 
   860 lemma ALG_PREFIXFREE_STEP: "ALL (l1::bool list list) l2::bool list list.
   861    alg_prefixfree (map (op # True) l1 @ map (op # False) l2) =
   862    (alg_prefixfree l1 & alg_prefixfree l2)"
   863   by (import prob_canon ALG_PREFIXFREE_STEP)
   864 
   865 lemma ALG_PREFIXFREE_APPEND: "ALL (h::bool list) (h'::bool list) (t::bool list list) t'::bool list list.
   866    alg_prefixfree ((h # t) @ h' # t') =
   867    (alg_prefixfree (h # t) &
   868     alg_prefixfree (h' # t') & ~ IS_PREFIX h' (last (h # t)))"
   869   by (import prob_canon ALG_PREFIXFREE_APPEND)
   870 
   871 lemma ALG_PREFIXFREE_FILTER: "ALL (P::bool list => bool) b::bool list list.
   872    alg_sorted b & alg_prefixfree b --> alg_prefixfree (filter P b)"
   873   by (import prob_canon ALG_PREFIXFREE_FILTER)
   874 
   875 lemma ALG_TWINFREE_TL: "ALL (h::bool list) t::bool list list.
   876    alg_twinfree (h # t) --> alg_twinfree t"
   877   by (import prob_canon ALG_TWINFREE_TL)
   878 
   879 lemma ALG_TWINFREE_TLS: "ALL (l::bool list list) b::bool.
   880    alg_twinfree (map (op # b) l) = alg_twinfree l"
   881   by (import prob_canon ALG_TWINFREE_TLS)
   882 
   883 lemma ALG_TWINFREE_STEP1: "ALL (l1::bool list list) l2::bool list list.
   884    alg_twinfree (map (op # True) l1 @ map (op # False) l2) -->
   885    alg_twinfree l1 & alg_twinfree l2"
   886   by (import prob_canon ALG_TWINFREE_STEP1)
   887 
   888 lemma ALG_TWINFREE_STEP2: "ALL (l1::bool list list) l2::bool list list.
   889    (~ [] mem l1 | ~ [] mem l2) & alg_twinfree l1 & alg_twinfree l2 -->
   890    alg_twinfree (map (op # True) l1 @ map (op # False) l2)"
   891   by (import prob_canon ALG_TWINFREE_STEP2)
   892 
   893 lemma ALG_TWINFREE_STEP: "ALL (l1::bool list list) l2::bool list list.
   894    ~ [] mem l1 | ~ [] mem l2 -->
   895    alg_twinfree (map (op # True) l1 @ map (op # False) l2) =
   896    (alg_twinfree l1 & alg_twinfree l2)"
   897   by (import prob_canon ALG_TWINFREE_STEP)
   898 
   899 lemma ALG_LONGEST_HD: "ALL (h::bool list) t::bool list list. length h <= alg_longest (h # t)"
   900   by (import prob_canon ALG_LONGEST_HD)
   901 
   902 lemma ALG_LONGEST_TL: "ALL (h::bool list) t::bool list list. alg_longest t <= alg_longest (h # t)"
   903   by (import prob_canon ALG_LONGEST_TL)
   904 
   905 lemma ALG_LONGEST_TLS: "ALL (h::bool list) (t::bool list list) b::bool.
   906    alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
   907   by (import prob_canon ALG_LONGEST_TLS)
   908 
   909 lemma ALG_LONGEST_APPEND: "ALL (l1::bool list list) l2::bool list list.
   910    alg_longest l1 <= alg_longest (l1 @ l2) &
   911    alg_longest l2 <= alg_longest (l1 @ l2)"
   912   by (import prob_canon ALG_LONGEST_APPEND)
   913 
   914 lemma ALG_CANON_PREFS_HD: "ALL (l::bool list) b::bool list list. hd (alg_canon_prefs l b) = l"
   915   by (import prob_canon ALG_CANON_PREFS_HD)
   916 
   917 lemma ALG_CANON_PREFS_DELETES: "ALL (l::bool list) (b::bool list list) x::bool list.
   918    x mem alg_canon_prefs l b --> x mem l # b"
   919   by (import prob_canon ALG_CANON_PREFS_DELETES)
   920 
   921 lemma ALG_CANON_PREFS_SORTED: "ALL (l::bool list) b::bool list list.
   922    alg_sorted (l # b) --> alg_sorted (alg_canon_prefs l b)"
   923   by (import prob_canon ALG_CANON_PREFS_SORTED)
   924 
   925 lemma ALG_CANON_PREFS_PREFIXFREE: "ALL (l::bool list) b::bool list list.
   926    alg_sorted b & alg_prefixfree b --> alg_prefixfree (alg_canon_prefs l b)"
   927   by (import prob_canon ALG_CANON_PREFS_PREFIXFREE)
   928 
   929 lemma ALG_CANON_PREFS_CONSTANT: "ALL (l::bool list) b::bool list list.
   930    alg_prefixfree (l # b) --> alg_canon_prefs l b = l # b"
   931   by (import prob_canon ALG_CANON_PREFS_CONSTANT)
   932 
   933 lemma ALG_CANON_FIND_HD: "ALL (l::bool list) (h::bool list) t::bool list list.
   934    hd (alg_canon_find l (h # t)) = l | hd (alg_canon_find l (h # t)) = h"
   935   by (import prob_canon ALG_CANON_FIND_HD)
   936 
   937 lemma ALG_CANON_FIND_DELETES: "ALL (l::bool list) (b::bool list list) x::bool list.
   938    x mem alg_canon_find l b --> x mem l # b"
   939   by (import prob_canon ALG_CANON_FIND_DELETES)
   940 
   941 lemma ALG_CANON_FIND_SORTED: "ALL (l::bool list) b::bool list list.
   942    alg_sorted b --> alg_sorted (alg_canon_find l b)"
   943   by (import prob_canon ALG_CANON_FIND_SORTED)
   944 
   945 lemma ALG_CANON_FIND_PREFIXFREE: "ALL (l::bool list) b::bool list list.
   946    alg_sorted b & alg_prefixfree b --> alg_prefixfree (alg_canon_find l b)"
   947   by (import prob_canon ALG_CANON_FIND_PREFIXFREE)
   948 
   949 lemma ALG_CANON_FIND_CONSTANT: "ALL (l::bool list) b::bool list list.
   950    alg_sorted (l # b) & alg_prefixfree (l # b) -->
   951    alg_canon_find l b = l # b"
   952   by (import prob_canon ALG_CANON_FIND_CONSTANT)
   953 
   954 lemma ALG_CANON1_SORTED: "ALL x::bool list list. alg_sorted (alg_canon1 x)"
   955   by (import prob_canon ALG_CANON1_SORTED)
   956 
   957 lemma ALG_CANON1_PREFIXFREE: "ALL l::bool list list. alg_prefixfree (alg_canon1 l)"
   958   by (import prob_canon ALG_CANON1_PREFIXFREE)
   959 
   960 lemma ALG_CANON1_CONSTANT: "ALL l::bool list list. alg_sorted l & alg_prefixfree l --> alg_canon1 l = l"
   961   by (import prob_canon ALG_CANON1_CONSTANT)
   962 
   963 lemma ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE: "ALL (l::bool list) b::bool list list.
   964    alg_sorted (l # b) & alg_prefixfree (l # b) & alg_twinfree b -->
   965    alg_sorted (alg_canon_merge l b) &
   966    alg_prefixfree (alg_canon_merge l b) & alg_twinfree (alg_canon_merge l b)"
   967   by (import prob_canon ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE)
   968 
   969 lemma ALG_CANON_MERGE_PREFIXFREE_PRESERVE: "ALL (l::bool list) (b::bool list list) h::bool list.
   970    (ALL x::bool list. x mem l # b --> ~ IS_PREFIX h x & ~ IS_PREFIX x h) -->
   971    (ALL x::bool list.
   972        x mem alg_canon_merge l b --> ~ IS_PREFIX h x & ~ IS_PREFIX x h)"
   973   by (import prob_canon ALG_CANON_MERGE_PREFIXFREE_PRESERVE)
   974 
   975 lemma ALG_CANON_MERGE_SHORTENS: "ALL (l::bool list) (b::bool list list) x::bool list.
   976    x mem alg_canon_merge l b -->
   977    (EX y::bool list. y mem l # b & IS_PREFIX y x)"
   978   by (import prob_canon ALG_CANON_MERGE_SHORTENS)
   979 
   980 lemma ALG_CANON_MERGE_CONSTANT: "ALL (l::bool list) b::bool list list.
   981    alg_twinfree (l # b) --> alg_canon_merge l b = l # b"
   982   by (import prob_canon ALG_CANON_MERGE_CONSTANT)
   983 
   984 lemma ALG_CANON2_PREFIXFREE_PRESERVE: "ALL (x::bool list list) xa::bool list.
   985    (ALL xb::bool list.
   986        xb mem x --> ~ IS_PREFIX xa xb & ~ IS_PREFIX xb xa) -->
   987    (ALL xb::bool list.
   988        xb mem alg_canon2 x --> ~ IS_PREFIX xa xb & ~ IS_PREFIX xb xa)"
   989   by (import prob_canon ALG_CANON2_PREFIXFREE_PRESERVE)
   990 
   991 lemma ALG_CANON2_SHORTENS: "ALL (x::bool list list) xa::bool list.
   992    xa mem alg_canon2 x --> (EX y::bool list. y mem x & IS_PREFIX y xa)"
   993   by (import prob_canon ALG_CANON2_SHORTENS)
   994 
   995 lemma ALG_CANON2_SORTED_PREFIXFREE_TWINFREE: "ALL x::bool list list.
   996    alg_sorted x & alg_prefixfree x -->
   997    alg_sorted (alg_canon2 x) &
   998    alg_prefixfree (alg_canon2 x) & alg_twinfree (alg_canon2 x)"
   999   by (import prob_canon ALG_CANON2_SORTED_PREFIXFREE_TWINFREE)
  1000 
  1001 lemma ALG_CANON2_CONSTANT: "ALL l::bool list list. alg_twinfree l --> alg_canon2 l = l"
  1002   by (import prob_canon ALG_CANON2_CONSTANT)
  1003 
  1004 lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l::bool list list.
  1005    alg_sorted (alg_canon l) &
  1006    alg_prefixfree (alg_canon l) & alg_twinfree (alg_canon l)"
  1007   by (import prob_canon ALG_CANON_SORTED_PREFIXFREE_TWINFREE)
  1008 
  1009 lemma ALG_CANON_CONSTANT: "ALL l::bool list list.
  1010    alg_sorted l & alg_prefixfree l & alg_twinfree l --> alg_canon l = l"
  1011   by (import prob_canon ALG_CANON_CONSTANT)
  1012 
  1013 lemma ALG_CANON_IDEMPOT: "ALL l::bool list list. alg_canon (alg_canon l) = alg_canon l"
  1014   by (import prob_canon ALG_CANON_IDEMPOT)
  1015 
  1016 lemma ALGEBRA_CANON_DEF_ALT: "ALL l::bool list list.
  1017    algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
  1018   by (import prob_canon ALGEBRA_CANON_DEF_ALT)
  1019 
  1020 lemma ALGEBRA_CANON_BASIC: "algebra_canon [] &
  1021 algebra_canon [[]] & (ALL x::bool list. algebra_canon [x])"
  1022   by (import prob_canon ALGEBRA_CANON_BASIC)
  1023 
  1024 lemma ALG_CANON_BASIC: "alg_canon [] = [] &
  1025 alg_canon [[]] = [[]] & (ALL x::bool list. alg_canon [x] = [x])"
  1026   by (import prob_canon ALG_CANON_BASIC)
  1027 
  1028 lemma ALGEBRA_CANON_TL: "ALL (h::bool list) t::bool list list.
  1029    algebra_canon (h # t) --> algebra_canon t"
  1030   by (import prob_canon ALGEBRA_CANON_TL)
  1031 
  1032 lemma ALGEBRA_CANON_NIL_MEM: "ALL l::bool list list. (algebra_canon l & [] mem l) = (l = [[]])"
  1033   by (import prob_canon ALGEBRA_CANON_NIL_MEM)
  1034 
  1035 lemma ALGEBRA_CANON_TLS: "ALL (l::bool list list) b::bool.
  1036    algebra_canon (map (op # b) l) = algebra_canon l"
  1037   by (import prob_canon ALGEBRA_CANON_TLS)
  1038 
  1039 lemma ALGEBRA_CANON_STEP1: "ALL (l1::bool list list) l2::bool list list.
  1040    algebra_canon (map (op # True) l1 @ map (op # False) l2) -->
  1041    algebra_canon l1 & algebra_canon l2"
  1042   by (import prob_canon ALGEBRA_CANON_STEP1)
  1043 
  1044 lemma ALGEBRA_CANON_STEP2: "ALL (l1::bool list list) l2::bool list list.
  1045    (l1 ~= [[]] | l2 ~= [[]]) & algebra_canon l1 & algebra_canon l2 -->
  1046    algebra_canon (map (op # True) l1 @ map (op # False) l2)"
  1047   by (import prob_canon ALGEBRA_CANON_STEP2)
  1048 
  1049 lemma ALGEBRA_CANON_STEP: "ALL (l1::bool list list) l2::bool list list.
  1050    l1 ~= [[]] | l2 ~= [[]] -->
  1051    algebra_canon (map (op # True) l1 @ map (op # False) l2) =
  1052    (algebra_canon l1 & algebra_canon l2)"
  1053   by (import prob_canon ALGEBRA_CANON_STEP)
  1054 
  1055 lemma ALGEBRA_CANON_CASES_THM: "ALL l::bool list list.
  1056    algebra_canon l -->
  1057    l = [] |
  1058    l = [[]] |
  1059    (EX (l1::bool list list) l2::bool list list.
  1060        algebra_canon l1 &
  1061        algebra_canon l2 & l = map (op # True) l1 @ map (op # False) l2)"
  1062   by (import prob_canon ALGEBRA_CANON_CASES_THM)
  1063 
  1064 lemma ALGEBRA_CANON_CASES: "ALL P::bool list list => bool.
  1065    P [] &
  1066    P [[]] &
  1067    (ALL (l1::bool list list) l2::bool list list.
  1068        algebra_canon l1 &
  1069        algebra_canon l2 &
  1070        algebra_canon (map (op # True) l1 @ map (op # False) l2) -->
  1071        P (map (op # True) l1 @ map (op # False) l2)) -->
  1072    (ALL l::bool list list. algebra_canon l --> P l)"
  1073   by (import prob_canon ALGEBRA_CANON_CASES)
  1074 
  1075 lemma ALGEBRA_CANON_INDUCTION: "ALL P::bool list list => bool.
  1076    P [] &
  1077    P [[]] &
  1078    (ALL (l1::bool list list) l2::bool list list.
  1079        algebra_canon l1 &
  1080        algebra_canon l2 &
  1081        P l1 &
  1082        P l2 & algebra_canon (map (op # True) l1 @ map (op # False) l2) -->
  1083        P (map (op # True) l1 @ map (op # False) l2)) -->
  1084    (ALL l::bool list list. algebra_canon l --> P l)"
  1085   by (import prob_canon ALGEBRA_CANON_INDUCTION)
  1086 
  1087 lemma MEM_NIL_STEP: "ALL (l1::bool list list) l2::bool list list.
  1088    ~ [] mem map (op # True) l1 @ map (op # False) l2"
  1089   by (import prob_canon MEM_NIL_STEP)
  1090 
  1091 lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l::bool list list.
  1092    (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
  1093   by (import prob_canon ALG_SORTED_PREFIXFREE_MEM_NIL)
  1094 
  1095 lemma ALG_SORTED_PREFIXFREE_EQUALITY: "ALL (l::bool list list) l'::bool list list.
  1096    (ALL x::bool list. x mem l = x mem l') &
  1097    alg_sorted l & alg_sorted l' & alg_prefixfree l & alg_prefixfree l' -->
  1098    l = l'"
  1099   by (import prob_canon ALG_SORTED_PREFIXFREE_EQUALITY)
  1100 
  1101 ;end_setup
  1102 
  1103 ;setup_theory boolean_sequence
  1104 
  1105 consts
  1106   SHD :: "(nat => bool) => bool" 
  1107 
  1108 defs
  1109   SHD_primdef: "SHD == %f::nat => bool. f 0"
  1110 
  1111 lemma SHD_def: "ALL f::nat => bool. SHD f = f 0"
  1112   by (import boolean_sequence SHD_def)
  1113 
  1114 consts
  1115   STL :: "(nat => bool) => nat => bool" 
  1116 
  1117 defs
  1118   STL_primdef: "STL == %(f::nat => bool) n::nat. f (Suc n)"
  1119 
  1120 lemma STL_def: "ALL (f::nat => bool) n::nat. STL f n = f (Suc n)"
  1121   by (import boolean_sequence STL_def)
  1122 
  1123 consts
  1124   SCONS :: "bool => (nat => bool) => nat => bool" 
  1125 
  1126 specification (SCONS_primdef: SCONS) SCONS_def: "(ALL (h::bool) t::nat => bool. SCONS h t 0 = h) &
  1127 (ALL (h::bool) (t::nat => bool) n::nat. SCONS h t (Suc n) = t n)"
  1128   by (import boolean_sequence SCONS_def)
  1129 
  1130 consts
  1131   SDEST :: "(nat => bool) => bool * (nat => bool)" 
  1132 
  1133 defs
  1134   SDEST_primdef: "SDEST == %s::nat => bool. (SHD s, STL s)"
  1135 
  1136 lemma SDEST_def: "SDEST = (%s::nat => bool. (SHD s, STL s))"
  1137   by (import boolean_sequence SDEST_def)
  1138 
  1139 consts
  1140   SCONST :: "bool => nat => bool" 
  1141 
  1142 defs
  1143   SCONST_primdef: "SCONST == K"
  1144 
  1145 lemma SCONST_def: "SCONST = K"
  1146   by (import boolean_sequence SCONST_def)
  1147 
  1148 consts
  1149   STAKE :: "nat => (nat => bool) => bool list" 
  1150 
  1151 specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s::nat => bool. STAKE 0 s = []) &
  1152 (ALL (n::nat) s::nat => bool. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
  1153   by (import boolean_sequence STAKE_def)
  1154 
  1155 consts
  1156   SDROP :: "nat => (nat => bool) => nat => bool" 
  1157 
  1158 specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n::nat. SDROP (Suc n) = SDROP n o STL)"
  1159   by (import boolean_sequence SDROP_def)
  1160 
  1161 lemma SCONS_SURJ: "ALL x::nat => bool. EX (xa::bool) t::nat => bool. x = SCONS xa t"
  1162   by (import boolean_sequence SCONS_SURJ)
  1163 
  1164 lemma SHD_STL_ISO: "ALL (h::bool) t::nat => bool. EX x::nat => bool. SHD x = h & STL x = t"
  1165   by (import boolean_sequence SHD_STL_ISO)
  1166 
  1167 lemma SHD_SCONS: "ALL (h::bool) t::nat => bool. SHD (SCONS h t) = h"
  1168   by (import boolean_sequence SHD_SCONS)
  1169 
  1170 lemma STL_SCONS: "ALL (h::bool) t::nat => bool. STL (SCONS h t) = t"
  1171   by (import boolean_sequence STL_SCONS)
  1172 
  1173 lemma SHD_SCONST: "ALL b::bool. SHD (SCONST b) = b"
  1174   by (import boolean_sequence SHD_SCONST)
  1175 
  1176 lemma STL_SCONST: "ALL b::bool. STL (SCONST b) = SCONST b"
  1177   by (import boolean_sequence STL_SCONST)
  1178 
  1179 ;end_setup
  1180 
  1181 ;setup_theory prob_algebra
  1182 
  1183 consts
  1184   alg_embed :: "bool list => (nat => bool) => bool" 
  1185 
  1186 specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s::nat => bool. alg_embed [] s = True) &
  1187 (ALL (h::bool) (t::bool list) s::nat => bool.
  1188     alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
  1189   by (import prob_algebra alg_embed_def)
  1190 
  1191 consts
  1192   algebra_embed :: "bool list list => (nat => bool) => bool" 
  1193 
  1194 specification (algebra_embed_primdef: algebra_embed) algebra_embed_def: "algebra_embed [] = EMPTY &
  1195 (ALL (h::bool list) t::bool list list.
  1196     algebra_embed (h # t) = pred_set.UNION (alg_embed h) (algebra_embed t))"
  1197   by (import prob_algebra algebra_embed_def)
  1198 
  1199 consts
  1200   measurable :: "((nat => bool) => bool) => bool" 
  1201 
  1202 defs
  1203   measurable_primdef: "measurable ==
  1204 %s::(nat => bool) => bool. EX b::bool list list. s = algebra_embed b"
  1205 
  1206 lemma measurable_def: "ALL s::(nat => bool) => bool.
  1207    measurable s = (EX b::bool list list. s = algebra_embed b)"
  1208   by (import prob_algebra measurable_def)
  1209 
  1210 lemma HALVES_INTER: "pred_set.INTER (%x::nat => bool. SHD x = True)
  1211  (%x::nat => bool. SHD x = False) =
  1212 EMPTY"
  1213   by (import prob_algebra HALVES_INTER)
  1214 
  1215 lemma INTER_STL: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
  1216    pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
  1217   by (import prob_algebra INTER_STL)
  1218 
  1219 lemma COMPL_SHD: "ALL b::bool.
  1220    COMPL (%x::nat => bool. SHD x = b) = (%x::nat => bool. SHD x = (~ b))"
  1221   by (import prob_algebra COMPL_SHD)
  1222 
  1223 lemma ALG_EMBED_BASIC: "alg_embed [] = pred_set.UNIV &
  1224 (ALL (h::bool) t::bool list.
  1225     alg_embed (h # t) =
  1226     pred_set.INTER (%x::nat => bool. SHD x = h) (alg_embed t o STL))"
  1227   by (import prob_algebra ALG_EMBED_BASIC)
  1228 
  1229 lemma ALG_EMBED_NIL: "ALL c::bool list. All (alg_embed c) = (c = [])"
  1230   by (import prob_algebra ALG_EMBED_NIL)
  1231 
  1232 lemma ALG_EMBED_POPULATED: "ALL b::bool list. Ex (alg_embed b)"
  1233   by (import prob_algebra ALG_EMBED_POPULATED)
  1234 
  1235 lemma ALG_EMBED_PREFIX: "ALL (b::bool list) (c::bool list) s::nat => bool.
  1236    alg_embed b s & alg_embed c s --> IS_PREFIX b c | IS_PREFIX c b"
  1237   by (import prob_algebra ALG_EMBED_PREFIX)
  1238 
  1239 lemma ALG_EMBED_PREFIX_SUBSET: "ALL (b::bool list) c::bool list.
  1240    SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
  1241   by (import prob_algebra ALG_EMBED_PREFIX_SUBSET)
  1242 
  1243 lemma ALG_EMBED_TWINS: "ALL l::bool list.
  1244    pred_set.UNION (alg_embed (SNOC True l)) (alg_embed (SNOC False l)) =
  1245    alg_embed l"
  1246   by (import prob_algebra ALG_EMBED_TWINS)
  1247 
  1248 lemma ALGEBRA_EMBED_BASIC: "algebra_embed [] = EMPTY &
  1249 algebra_embed [[]] = pred_set.UNIV &
  1250 (ALL b::bool. algebra_embed [[b]] = (%s::nat => bool. SHD s = b))"
  1251   by (import prob_algebra ALGEBRA_EMBED_BASIC)
  1252 
  1253 lemma ALGEBRA_EMBED_MEM: "ALL (b::bool list list) x::nat => bool.
  1254    algebra_embed b x --> (EX l::bool list. l mem b & alg_embed l x)"
  1255   by (import prob_algebra ALGEBRA_EMBED_MEM)
  1256 
  1257 lemma ALGEBRA_EMBED_APPEND: "ALL (l1::bool list list) l2::bool list list.
  1258    algebra_embed (l1 @ l2) =
  1259    pred_set.UNION (algebra_embed l1) (algebra_embed l2)"
  1260   by (import prob_algebra ALGEBRA_EMBED_APPEND)
  1261 
  1262 lemma ALGEBRA_EMBED_TLS: "ALL (l::bool list list) b::bool.
  1263    algebra_embed (map (op # b) l) (SCONS (h::bool) (t::nat => bool)) =
  1264    (h = b & algebra_embed l t)"
  1265   by (import prob_algebra ALGEBRA_EMBED_TLS)
  1266 
  1267 lemma ALG_CANON_PREFS_EMBED: "ALL (l::bool list) b::bool list list.
  1268    algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
  1269   by (import prob_algebra ALG_CANON_PREFS_EMBED)
  1270 
  1271 lemma ALG_CANON_FIND_EMBED: "ALL (l::bool list) b::bool list list.
  1272    algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
  1273   by (import prob_algebra ALG_CANON_FIND_EMBED)
  1274 
  1275 lemma ALG_CANON1_EMBED: "ALL x::bool list list. algebra_embed (alg_canon1 x) = algebra_embed x"
  1276   by (import prob_algebra ALG_CANON1_EMBED)
  1277 
  1278 lemma ALG_CANON_MERGE_EMBED: "ALL (l::bool list) b::bool list list.
  1279    algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
  1280   by (import prob_algebra ALG_CANON_MERGE_EMBED)
  1281 
  1282 lemma ALG_CANON2_EMBED: "ALL x::bool list list. algebra_embed (alg_canon2 x) = algebra_embed x"
  1283   by (import prob_algebra ALG_CANON2_EMBED)
  1284 
  1285 lemma ALG_CANON_EMBED: "ALL l::bool list list. algebra_embed (alg_canon l) = algebra_embed l"
  1286   by (import prob_algebra ALG_CANON_EMBED)
  1287 
  1288 lemma ALGEBRA_CANON_UNIV: "ALL l::bool list list.
  1289    algebra_canon l --> algebra_embed l = pred_set.UNIV --> l = [[]]"
  1290   by (import prob_algebra ALGEBRA_CANON_UNIV)
  1291 
  1292 lemma ALG_CANON_REP: "ALL (b::bool list list) c::bool list list.
  1293    (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
  1294   by (import prob_algebra ALG_CANON_REP)
  1295 
  1296 lemma ALGEBRA_CANON_EMBED_EMPTY: "ALL l::bool list list.
  1297    algebra_canon l --> (ALL v::nat => bool. ~ algebra_embed l v) = (l = [])"
  1298   by (import prob_algebra ALGEBRA_CANON_EMBED_EMPTY)
  1299 
  1300 lemma ALGEBRA_CANON_EMBED_UNIV: "ALL l::bool list list.
  1301    algebra_canon l --> All (algebra_embed l) = (l = [[]])"
  1302   by (import prob_algebra ALGEBRA_CANON_EMBED_UNIV)
  1303 
  1304 lemma MEASURABLE_ALGEBRA: "ALL b::bool list list. measurable (algebra_embed b)"
  1305   by (import prob_algebra MEASURABLE_ALGEBRA)
  1306 
  1307 lemma MEASURABLE_BASIC: "measurable EMPTY &
  1308 measurable pred_set.UNIV &
  1309 (ALL b::bool. measurable (%s::nat => bool. SHD s = b))"
  1310   by (import prob_algebra MEASURABLE_BASIC)
  1311 
  1312 lemma MEASURABLE_SHD: "ALL b::bool. measurable (%s::nat => bool. SHD s = b)"
  1313   by (import prob_algebra MEASURABLE_SHD)
  1314 
  1315 lemma ALGEBRA_EMBED_COMPL: "ALL l::bool list list.
  1316    EX l'::bool list list. COMPL (algebra_embed l) = algebra_embed l'"
  1317   by (import prob_algebra ALGEBRA_EMBED_COMPL)
  1318 
  1319 lemma MEASURABLE_COMPL: "ALL s::(nat => bool) => bool. measurable (COMPL s) = measurable s"
  1320   by (import prob_algebra MEASURABLE_COMPL)
  1321 
  1322 lemma MEASURABLE_UNION: "ALL (s::(nat => bool) => bool) t::(nat => bool) => bool.
  1323    measurable s & measurable t --> measurable (pred_set.UNION s t)"
  1324   by (import prob_algebra MEASURABLE_UNION)
  1325 
  1326 lemma MEASURABLE_INTER: "ALL (s::(nat => bool) => bool) t::(nat => bool) => bool.
  1327    measurable s & measurable t --> measurable (pred_set.INTER s t)"
  1328   by (import prob_algebra MEASURABLE_INTER)
  1329 
  1330 lemma MEASURABLE_STL: "ALL p::(nat => bool) => bool. measurable (p o STL) = measurable p"
  1331   by (import prob_algebra MEASURABLE_STL)
  1332 
  1333 lemma MEASURABLE_SDROP: "ALL (n::nat) p::(nat => bool) => bool.
  1334    measurable (p o SDROP n) = measurable p"
  1335   by (import prob_algebra MEASURABLE_SDROP)
  1336 
  1337 lemma MEASURABLE_INTER_HALVES: "ALL p::(nat => bool) => bool.
  1338    (measurable (pred_set.INTER (%x::nat => bool. SHD x = True) p) &
  1339     measurable (pred_set.INTER (%x::nat => bool. SHD x = False) p)) =
  1340    measurable p"
  1341   by (import prob_algebra MEASURABLE_INTER_HALVES)
  1342 
  1343 lemma MEASURABLE_HALVES: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
  1344    measurable
  1345     (pred_set.UNION (pred_set.INTER (%x::nat => bool. SHD x = True) p)
  1346       (pred_set.INTER (%x::nat => bool. SHD x = False) q)) =
  1347    (measurable (pred_set.INTER (%x::nat => bool. SHD x = True) p) &
  1348     measurable (pred_set.INTER (%x::nat => bool. SHD x = False) q))"
  1349   by (import prob_algebra MEASURABLE_HALVES)
  1350 
  1351 lemma MEASURABLE_INTER_SHD: "ALL (b::bool) p::(nat => bool) => bool.
  1352    measurable (pred_set.INTER (%x::nat => bool. SHD x = b) (p o STL)) =
  1353    measurable p"
  1354   by (import prob_algebra MEASURABLE_INTER_SHD)
  1355 
  1356 ;end_setup
  1357 
  1358 ;setup_theory prob
  1359 
  1360 consts
  1361   alg_measure :: "bool list list => real" 
  1362 
  1363 specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
  1364 (ALL (l::bool list) rest::bool list list.
  1365     alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
  1366   by (import prob alg_measure_def)
  1367 
  1368 consts
  1369   algebra_measure :: "bool list list => real" 
  1370 
  1371 defs
  1372   algebra_measure_primdef: "algebra_measure ==
  1373 %b::bool list list.
  1374    inf (%r::real.
  1375            EX c::bool list list.
  1376               algebra_embed b = algebra_embed c & alg_measure c = r)"
  1377 
  1378 lemma algebra_measure_def: "ALL b::bool list list.
  1379    algebra_measure b =
  1380    inf (%r::real.
  1381            EX c::bool list list.
  1382               algebra_embed b = algebra_embed c & alg_measure c = r)"
  1383   by (import prob algebra_measure_def)
  1384 
  1385 consts
  1386   prob :: "((nat => bool) => bool) => real" 
  1387 
  1388 defs
  1389   prob_primdef: "prob ==
  1390 %s::(nat => bool) => bool.
  1391    sup (%r::real.
  1392            EX b::bool list list.
  1393               algebra_measure b = r & SUBSET (algebra_embed b) s)"
  1394 
  1395 lemma prob_def: "ALL s::(nat => bool) => bool.
  1396    prob s =
  1397    sup (%r::real.
  1398            EX b::bool list list.
  1399               algebra_measure b = r & SUBSET (algebra_embed b) s)"
  1400   by (import prob prob_def)
  1401 
  1402 lemma ALG_TWINS_MEASURE: "(All::(bool list => bool) => bool)
  1403  (%l::bool list.
  1404      (op =::real => real => bool)
  1405       ((op +::real => real => real)
  1406         ((op ^::real => nat => real)
  1407           ((op /::real => real => real) (1::real)
  1408             ((number_of::bin => real)
  1409               ((op BIT::bin => bit => bin)
  1410                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
  1411                   (bit.B1::bit))
  1412                 (bit.B0::bit))))
  1413           ((size::bool list => nat)
  1414             ((SNOC::bool => bool list => bool list) (True::bool) l)))
  1415         ((op ^::real => nat => real)
  1416           ((op /::real => real => real) (1::real)
  1417             ((number_of::bin => real)
  1418               ((op BIT::bin => bit => bin)
  1419                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
  1420                   (bit.B1::bit))
  1421                 (bit.B0::bit))))
  1422           ((size::bool list => nat)
  1423             ((SNOC::bool => bool list => bool list) (False::bool) l))))
  1424       ((op ^::real => nat => real)
  1425         ((op /::real => real => real) (1::real)
  1426           ((number_of::bin => real)
  1427             ((op BIT::bin => bit => bin)
  1428               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
  1429               (bit.B0::bit))))
  1430         ((size::bool list => nat) l)))"
  1431   by (import prob ALG_TWINS_MEASURE)
  1432 
  1433 lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
  1434 alg_measure [[]] = 1 & (ALL b::bool. alg_measure [[b]] = 1 / 2)"
  1435   by (import prob ALG_MEASURE_BASIC)
  1436 
  1437 lemma ALG_MEASURE_POS: "ALL l::bool list list. 0 <= alg_measure l"
  1438   by (import prob ALG_MEASURE_POS)
  1439 
  1440 lemma ALG_MEASURE_APPEND: "ALL (l1::bool list list) l2::bool list list.
  1441    alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
  1442   by (import prob ALG_MEASURE_APPEND)
  1443 
  1444 lemma ALG_MEASURE_TLS: "ALL (l::bool list list) b::bool.
  1445    2 * alg_measure (map (op # b) l) = alg_measure l"
  1446   by (import prob ALG_MEASURE_TLS)
  1447 
  1448 lemma ALG_CANON_PREFS_MONO: "ALL (l::bool list) b::bool list list.
  1449    alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
  1450   by (import prob ALG_CANON_PREFS_MONO)
  1451 
  1452 lemma ALG_CANON_FIND_MONO: "ALL (l::bool list) b::bool list list.
  1453    alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
  1454   by (import prob ALG_CANON_FIND_MONO)
  1455 
  1456 lemma ALG_CANON1_MONO: "ALL x::bool list list. alg_measure (alg_canon1 x) <= alg_measure x"
  1457   by (import prob ALG_CANON1_MONO)
  1458 
  1459 lemma ALG_CANON_MERGE_MONO: "ALL (l::bool list) b::bool list list.
  1460    alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
  1461   by (import prob ALG_CANON_MERGE_MONO)
  1462 
  1463 lemma ALG_CANON2_MONO: "ALL x::bool list list. alg_measure (alg_canon2 x) <= alg_measure x"
  1464   by (import prob ALG_CANON2_MONO)
  1465 
  1466 lemma ALG_CANON_MONO: "ALL l::bool list list. alg_measure (alg_canon l) <= alg_measure l"
  1467   by (import prob ALG_CANON_MONO)
  1468 
  1469 lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l::bool list list. algebra_measure l = alg_measure (alg_canon l)"
  1470   by (import prob ALGEBRA_MEASURE_DEF_ALT)
  1471 
  1472 lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
  1473 algebra_measure [[]] = 1 & (ALL b::bool. algebra_measure [[b]] = 1 / 2)"
  1474   by (import prob ALGEBRA_MEASURE_BASIC)
  1475 
  1476 lemma ALGEBRA_CANON_MEASURE_MAX: "ALL l::bool list list. algebra_canon l --> alg_measure l <= 1"
  1477   by (import prob ALGEBRA_CANON_MEASURE_MAX)
  1478 
  1479 lemma ALGEBRA_MEASURE_MAX: "ALL l::bool list list. algebra_measure l <= 1"
  1480   by (import prob ALGEBRA_MEASURE_MAX)
  1481 
  1482 lemma ALGEBRA_MEASURE_MONO_EMBED: "ALL (x::bool list list) xa::bool list list.
  1483    SUBSET (algebra_embed x) (algebra_embed xa) -->
  1484    algebra_measure x <= algebra_measure xa"
  1485   by (import prob ALGEBRA_MEASURE_MONO_EMBED)
  1486 
  1487 lemma ALG_MEASURE_COMPL: "ALL l::bool list list.
  1488    algebra_canon l -->
  1489    (ALL c::bool list list.
  1490        algebra_canon c -->
  1491        COMPL (algebra_embed l) = algebra_embed c -->
  1492        alg_measure l + alg_measure c = 1)"
  1493   by (import prob ALG_MEASURE_COMPL)
  1494 
  1495 lemma ALG_MEASURE_ADDITIVE: "ALL l::bool list list.
  1496    algebra_canon l -->
  1497    (ALL c::bool list list.
  1498        algebra_canon c -->
  1499        (ALL d::bool list list.
  1500            algebra_canon d -->
  1501            pred_set.INTER (algebra_embed c) (algebra_embed d) = EMPTY &
  1502            algebra_embed l =
  1503            pred_set.UNION (algebra_embed c) (algebra_embed d) -->
  1504            alg_measure l = alg_measure c + alg_measure d))"
  1505   by (import prob ALG_MEASURE_ADDITIVE)
  1506 
  1507 lemma PROB_ALGEBRA: "ALL l::bool list list. prob (algebra_embed l) = algebra_measure l"
  1508   by (import prob PROB_ALGEBRA)
  1509 
  1510 lemma PROB_BASIC: "prob EMPTY = 0 &
  1511 prob pred_set.UNIV = 1 &
  1512 (ALL b::bool. prob (%s::nat => bool. SHD s = b) = 1 / 2)"
  1513   by (import prob PROB_BASIC)
  1514 
  1515 lemma PROB_ADDITIVE: "ALL (s::(nat => bool) => bool) t::(nat => bool) => bool.
  1516    measurable s & measurable t & pred_set.INTER s t = EMPTY -->
  1517    prob (pred_set.UNION s t) = prob s + prob t"
  1518   by (import prob PROB_ADDITIVE)
  1519 
  1520 lemma PROB_COMPL: "ALL s::(nat => bool) => bool. measurable s --> prob (COMPL s) = 1 - prob s"
  1521   by (import prob PROB_COMPL)
  1522 
  1523 lemma PROB_SUP_EXISTS1: "ALL s::(nat => bool) => bool.
  1524    EX (x::real) b::bool list list.
  1525       algebra_measure b = x & SUBSET (algebra_embed b) s"
  1526   by (import prob PROB_SUP_EXISTS1)
  1527 
  1528 lemma PROB_SUP_EXISTS2: "ALL s::(nat => bool) => bool.
  1529    EX x::real.
  1530       ALL r::real.
  1531          (EX b::bool list list.
  1532              algebra_measure b = r & SUBSET (algebra_embed b) s) -->
  1533          r <= x"
  1534   by (import prob PROB_SUP_EXISTS2)
  1535 
  1536 lemma PROB_LE_X: "ALL (s::(nat => bool) => bool) x::real.
  1537    (ALL s'::(nat => bool) => bool.
  1538        measurable s' & SUBSET s' s --> prob s' <= x) -->
  1539    prob s <= x"
  1540   by (import prob PROB_LE_X)
  1541 
  1542 lemma X_LE_PROB: "ALL (s::(nat => bool) => bool) x::real.
  1543    (EX s'::(nat => bool) => bool.
  1544        measurable s' & SUBSET s' s & x <= prob s') -->
  1545    x <= prob s"
  1546   by (import prob X_LE_PROB)
  1547 
  1548 lemma PROB_SUBSET_MONO: "ALL (s::(nat => bool) => bool) t::(nat => bool) => bool.
  1549    SUBSET s t --> prob s <= prob t"
  1550   by (import prob PROB_SUBSET_MONO)
  1551 
  1552 lemma PROB_ALG: "ALL x::bool list. prob (alg_embed x) = (1 / 2) ^ length x"
  1553   by (import prob PROB_ALG)
  1554 
  1555 lemma PROB_STL: "ALL p::(nat => bool) => bool. measurable p --> prob (p o STL) = prob p"
  1556   by (import prob PROB_STL)
  1557 
  1558 lemma PROB_SDROP: "ALL (n::nat) p::(nat => bool) => bool.
  1559    measurable p --> prob (p o SDROP n) = prob p"
  1560   by (import prob PROB_SDROP)
  1561 
  1562 lemma PROB_INTER_HALVES: "ALL p::(nat => bool) => bool.
  1563    measurable p -->
  1564    prob (pred_set.INTER (%x::nat => bool. SHD x = True) p) +
  1565    prob (pred_set.INTER (%x::nat => bool. SHD x = False) p) =
  1566    prob p"
  1567   by (import prob PROB_INTER_HALVES)
  1568 
  1569 lemma PROB_INTER_SHD: "ALL (b::bool) p::(nat => bool) => bool.
  1570    measurable p -->
  1571    prob (pred_set.INTER (%x::nat => bool. SHD x = b) (p o STL)) =
  1572    1 / 2 * prob p"
  1573   by (import prob PROB_INTER_SHD)
  1574 
  1575 lemma ALGEBRA_MEASURE_POS: "ALL l::bool list list. 0 <= algebra_measure l"
  1576   by (import prob ALGEBRA_MEASURE_POS)
  1577 
  1578 lemma ALGEBRA_MEASURE_RANGE: "ALL l::bool list list. 0 <= algebra_measure l & algebra_measure l <= 1"
  1579   by (import prob ALGEBRA_MEASURE_RANGE)
  1580 
  1581 lemma PROB_POS: "ALL p::(nat => bool) => bool. 0 <= prob p"
  1582   by (import prob PROB_POS)
  1583 
  1584 lemma PROB_MAX: "ALL p::(nat => bool) => bool. prob p <= 1"
  1585   by (import prob PROB_MAX)
  1586 
  1587 lemma PROB_RANGE: "ALL p::(nat => bool) => bool. 0 <= prob p & prob p <= 1"
  1588   by (import prob PROB_RANGE)
  1589 
  1590 lemma ABS_PROB: "ALL p::(nat => bool) => bool. abs (prob p) = prob p"
  1591   by (import prob ABS_PROB)
  1592 
  1593 lemma PROB_SHD: "ALL b::bool. prob (%s::nat => bool. SHD s = b) = 1 / 2"
  1594   by (import prob PROB_SHD)
  1595 
  1596 lemma PROB_COMPL_LE1: "ALL (p::(nat => bool) => bool) r::real.
  1597    measurable p --> (prob (COMPL p) <= r) = (1 - r <= prob p)"
  1598   by (import prob PROB_COMPL_LE1)
  1599 
  1600 ;end_setup
  1601 
  1602 ;setup_theory prob_pseudo
  1603 
  1604 consts
  1605   pseudo_linear_hd :: "nat => bool" 
  1606 
  1607 defs
  1608   pseudo_linear_hd_primdef: "pseudo_linear_hd == EVEN"
  1609 
  1610 lemma pseudo_linear_hd_def: "pseudo_linear_hd = EVEN"
  1611   by (import prob_pseudo pseudo_linear_hd_def)
  1612 
  1613 consts
  1614   pseudo_linear_tl :: "nat => nat => nat => nat => nat" 
  1615 
  1616 defs
  1617   pseudo_linear_tl_primdef: "pseudo_linear_tl ==
  1618 %(a::nat) (b::nat) (n::nat) x::nat. (a * x + b) mod (2 * n + 1)"
  1619 
  1620 lemma pseudo_linear_tl_def: "ALL (a::nat) (b::nat) (n::nat) x::nat.
  1621    pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
  1622   by (import prob_pseudo pseudo_linear_tl_def)
  1623 
  1624 lemma PSEUDO_LINEAR1_EXECUTE: "EX x::nat => nat => bool.
  1625    (ALL xa::nat. SHD (x xa) = pseudo_linear_hd xa) &
  1626    (ALL xa::nat.
  1627        STL (x xa) =
  1628        x (pseudo_linear_tl
  1629            (NUMERAL
  1630              (NUMERAL_BIT1
  1631                (NUMERAL_BIT1
  1632                  (NUMERAL_BIT1
  1633                    (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1634            (NUMERAL
  1635              (NUMERAL_BIT1
  1636                (NUMERAL_BIT1
  1637                  (NUMERAL_BIT1
  1638                    (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1639            (NUMERAL
  1640              (NUMERAL_BIT1
  1641                (NUMERAL_BIT1
  1642                  (NUMERAL_BIT1
  1643                    (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  1644            xa))"
  1645   by (import prob_pseudo PSEUDO_LINEAR1_EXECUTE)
  1646 
  1647 consts
  1648   pseudo_linear1 :: "nat => nat => bool" 
  1649 
  1650 specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x::nat. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
  1651 (ALL x::nat.
  1652     STL (pseudo_linear1 x) =
  1653     pseudo_linear1
  1654      (pseudo_linear_tl
  1655        (NUMERAL
  1656          (NUMERAL_BIT1
  1657            (NUMERAL_BIT1
  1658              (NUMERAL_BIT1
  1659                (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1660        (NUMERAL
  1661          (NUMERAL_BIT1
  1662            (NUMERAL_BIT1
  1663              (NUMERAL_BIT1
  1664                (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  1665        (NUMERAL
  1666          (NUMERAL_BIT1
  1667            (NUMERAL_BIT1
  1668              (NUMERAL_BIT1
  1669                (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  1670        x))"
  1671   by (import prob_pseudo pseudo_linear1_def)
  1672 
  1673 consts
  1674   pseudo :: "nat => nat => bool" 
  1675 
  1676 defs
  1677   pseudo_primdef: "pseudo == pseudo_linear1"
  1678 
  1679 lemma pseudo_def: "pseudo = pseudo_linear1"
  1680   by (import prob_pseudo pseudo_def)
  1681 
  1682 ;end_setup
  1683 
  1684 ;setup_theory prob_indep
  1685 
  1686 consts
  1687   indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool" 
  1688 
  1689 defs
  1690   indep_set_primdef: "indep_set ==
  1691 %(p::(nat => bool) => bool) q::(nat => bool) => bool.
  1692    measurable p & measurable q & prob (pred_set.INTER p q) = prob p * prob q"
  1693 
  1694 lemma indep_set_def: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
  1695    indep_set p q =
  1696    (measurable p &
  1697     measurable q & prob (pred_set.INTER p q) = prob p * prob q)"
  1698   by (import prob_indep indep_set_def)
  1699 
  1700 consts
  1701   alg_cover_set :: "bool list list => bool" 
  1702 
  1703 defs
  1704   alg_cover_set_primdef: "alg_cover_set ==
  1705 %l::bool list list.
  1706    alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
  1707 
  1708 lemma alg_cover_set_def: "ALL l::bool list list.
  1709    alg_cover_set l =
  1710    (alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV)"
  1711   by (import prob_indep alg_cover_set_def)
  1712 
  1713 consts
  1714   alg_cover :: "bool list list => (nat => bool) => bool list" 
  1715 
  1716 defs
  1717   alg_cover_primdef: "alg_cover ==
  1718 %(l::bool list list) x::nat => bool.
  1719    SOME b::bool list. b mem l & alg_embed b x"
  1720 
  1721 lemma alg_cover_def: "ALL (l::bool list list) x::nat => bool.
  1722    alg_cover l x = (SOME b::bool list. b mem l & alg_embed b x)"
  1723   by (import prob_indep alg_cover_def)
  1724 
  1725 consts
  1726   indep :: "((nat => bool) => 'a * (nat => bool)) => bool" 
  1727 
  1728 defs
  1729   indep_primdef: "indep ==
  1730 %f::(nat => bool) => 'a::type * (nat => bool).
  1731    EX (l::bool list list) r::bool list => 'a::type.
  1732       alg_cover_set l &
  1733       (ALL s::nat => bool.
  1734           f s =
  1735           (let c::bool list = alg_cover l s in (r c, SDROP (length c) s)))"
  1736 
  1737 lemma indep_def: "ALL f::(nat => bool) => 'a::type * (nat => bool).
  1738    indep f =
  1739    (EX (l::bool list list) r::bool list => 'a::type.
  1740        alg_cover_set l &
  1741        (ALL s::nat => bool.
  1742            f s =
  1743            (let c::bool list = alg_cover l s in (r c, SDROP (length c) s))))"
  1744   by (import prob_indep indep_def)
  1745 
  1746 lemma INDEP_SET_BASIC: "ALL p::(nat => bool) => bool.
  1747    measurable p --> indep_set EMPTY p & indep_set pred_set.UNIV p"
  1748   by (import prob_indep INDEP_SET_BASIC)
  1749 
  1750 lemma INDEP_SET_SYM: "ALL (p::(nat => bool) => bool) q::(nat => bool) => bool.
  1751    indep_set p q = indep_set p q"
  1752   by (import prob_indep INDEP_SET_SYM)
  1753 
  1754 lemma INDEP_SET_DISJOINT_DECOMP: "ALL (p::(nat => bool) => bool) (q::(nat => bool) => bool)
  1755    r::(nat => bool) => bool.
  1756    indep_set p r & indep_set q r & pred_set.INTER p q = EMPTY -->
  1757    indep_set (pred_set.UNION p q) r"
  1758   by (import prob_indep INDEP_SET_DISJOINT_DECOMP)
  1759 
  1760 lemma ALG_COVER_SET_BASIC: "~ alg_cover_set [] & alg_cover_set [[]] & alg_cover_set [[True], [False]]"
  1761   by (import prob_indep ALG_COVER_SET_BASIC)
  1762 
  1763 lemma ALG_COVER_WELL_DEFINED: "ALL (l::bool list list) x::nat => bool.
  1764    alg_cover_set l --> alg_cover l x mem l & alg_embed (alg_cover l x) x"
  1765   by (import prob_indep ALG_COVER_WELL_DEFINED)
  1766 
  1767 lemma ALG_COVER_UNIV: "alg_cover [[]] = K []"
  1768   by (import prob_indep ALG_COVER_UNIV)
  1769 
  1770 lemma MAP_CONS_TL_FILTER: "ALL (l::bool list list) b::bool.
  1771    ~ [] mem l -->
  1772    map (op # b) (map tl [x::bool list:l. hd x = b]) =
  1773    [x::bool list:l. hd x = b]"
  1774   by (import prob_indep MAP_CONS_TL_FILTER)
  1775 
  1776 lemma ALG_COVER_SET_CASES_THM: "ALL l::bool list list.
  1777    alg_cover_set l =
  1778    (l = [[]] |
  1779     (EX (x::bool list list) xa::bool list list.
  1780         alg_cover_set x &
  1781         alg_cover_set xa & l = map (op # True) x @ map (op # False) xa))"
  1782   by (import prob_indep ALG_COVER_SET_CASES_THM)
  1783 
  1784 lemma ALG_COVER_SET_CASES: "ALL P::bool list list => bool.
  1785    P [[]] &
  1786    (ALL (l1::bool list list) l2::bool list list.
  1787        alg_cover_set l1 &
  1788        alg_cover_set l2 &
  1789        alg_cover_set (map (op # True) l1 @ map (op # False) l2) -->
  1790        P (map (op # True) l1 @ map (op # False) l2)) -->
  1791    (ALL l::bool list list. alg_cover_set l --> P l)"
  1792   by (import prob_indep ALG_COVER_SET_CASES)
  1793 
  1794 lemma ALG_COVER_SET_INDUCTION: "ALL P::bool list list => bool.
  1795    P [[]] &
  1796    (ALL (l1::bool list list) l2::bool list list.
  1797        alg_cover_set l1 &
  1798        alg_cover_set l2 &
  1799        P l1 &
  1800        P l2 & alg_cover_set (map (op # True) l1 @ map (op # False) l2) -->
  1801        P (map (op # True) l1 @ map (op # False) l2)) -->
  1802    (ALL l::bool list list. alg_cover_set l --> P l)"
  1803   by (import prob_indep ALG_COVER_SET_INDUCTION)
  1804 
  1805 lemma ALG_COVER_EXISTS_UNIQUE: "ALL l::bool list list.
  1806    alg_cover_set l -->
  1807    (ALL s::nat => bool. EX! x::bool list. x mem l & alg_embed x s)"
  1808   by (import prob_indep ALG_COVER_EXISTS_UNIQUE)
  1809 
  1810 lemma ALG_COVER_UNIQUE: "ALL (l::bool list list) (x::bool list) s::nat => bool.
  1811    alg_cover_set l & x mem l & alg_embed x s --> alg_cover l s = x"
  1812   by (import prob_indep ALG_COVER_UNIQUE)
  1813 
  1814 lemma ALG_COVER_STEP: "ALL (l1::bool list list) (l2::bool list list) (h::bool) t::nat => bool.
  1815    alg_cover_set l1 & alg_cover_set l2 -->
  1816    alg_cover (map (op # True) l1 @ map (op # False) l2) (SCONS h t) =
  1817    (if h then True # alg_cover l1 t else False # alg_cover l2 t)"
  1818   by (import prob_indep ALG_COVER_STEP)
  1819 
  1820 lemma ALG_COVER_HEAD: "ALL l::bool list list.
  1821    alg_cover_set l -->
  1822    (ALL f::bool list => bool. f o alg_cover l = algebra_embed (filter f l))"
  1823   by (import prob_indep ALG_COVER_HEAD)
  1824 
  1825 lemma ALG_COVER_TAIL_STEP: "ALL (l1::bool list list) (l2::bool list list) q::(nat => bool) => bool.
  1826    alg_cover_set l1 & alg_cover_set l2 -->
  1827    q o
  1828    (%x::nat => bool.
  1829        SDROP
  1830         (length (alg_cover (map (op # True) l1 @ map (op # False) l2) x))
  1831         x) =
  1832    pred_set.UNION
  1833     (pred_set.INTER (%x::nat => bool. SHD x = True)
  1834       (q o ((%x::nat => bool. SDROP (length (alg_cover l1 x)) x) o STL)))
  1835     (pred_set.INTER (%x::nat => bool. SHD x = False)
  1836       (q o ((%x::nat => bool. SDROP (length (alg_cover l2 x)) x) o STL)))"
  1837   by (import prob_indep ALG_COVER_TAIL_STEP)
  1838 
  1839 lemma ALG_COVER_TAIL_MEASURABLE: "ALL l::bool list list.
  1840    alg_cover_set l -->
  1841    (ALL q::(nat => bool) => bool.
  1842        measurable
  1843         (q o (%x::nat => bool. SDROP (length (alg_cover l x)) x)) =
  1844        measurable q)"
  1845   by (import prob_indep ALG_COVER_TAIL_MEASURABLE)
  1846 
  1847 lemma ALG_COVER_TAIL_PROB: "ALL l::bool list list.
  1848    alg_cover_set l -->
  1849    (ALL q::(nat => bool) => bool.
  1850        measurable q -->
  1851        prob (q o (%x::nat => bool. SDROP (length (alg_cover l x)) x)) =
  1852        prob q)"
  1853   by (import prob_indep ALG_COVER_TAIL_PROB)
  1854 
  1855 lemma INDEP_INDEP_SET_LEMMA: "ALL l::bool list list.
  1856    alg_cover_set l -->
  1857    (ALL q::(nat => bool) => bool.
  1858        measurable q -->
  1859        (ALL x::bool list.
  1860            x mem l -->
  1861            prob
  1862             (pred_set.INTER (alg_embed x)
  1863               (q o (%x::nat => bool. SDROP (length (alg_cover l x)) x))) =
  1864            (1 / 2) ^ length x * prob q))"
  1865   by (import prob_indep INDEP_INDEP_SET_LEMMA)
  1866 
  1867 lemma INDEP_SET_LIST: "ALL (q::(nat => bool) => bool) l::bool list list.
  1868    alg_sorted l &
  1869    alg_prefixfree l &
  1870    measurable q &
  1871    (ALL x::bool list. x mem l --> indep_set (alg_embed x) q) -->
  1872    indep_set (algebra_embed l) q"
  1873   by (import prob_indep INDEP_SET_LIST)
  1874 
  1875 lemma INDEP_INDEP_SET: "ALL (f::(nat => bool) => 'a::type * (nat => bool)) (p::'a::type => bool)
  1876    q::(nat => bool) => bool.
  1877    indep f & measurable q --> indep_set (p o (fst o f)) (q o (snd o f))"
  1878   by (import prob_indep INDEP_INDEP_SET)
  1879 
  1880 lemma INDEP_UNIT: "ALL x::'a::type. indep (UNIT x)"
  1881   by (import prob_indep INDEP_UNIT)
  1882 
  1883 lemma INDEP_SDEST: "indep SDEST"
  1884   by (import prob_indep INDEP_SDEST)
  1885 
  1886 lemma BIND_STEP: "ALL f::(nat => bool) => 'a::type * (nat => bool).
  1887    BIND SDEST (%k::bool. f o SCONS k) = f"
  1888   by (import prob_indep BIND_STEP)
  1889 
  1890 lemma INDEP_BIND_SDEST: "ALL f::bool => (nat => bool) => 'a::type * (nat => bool).
  1891    (ALL x::bool. indep (f x)) --> indep (BIND SDEST f)"
  1892   by (import prob_indep INDEP_BIND_SDEST)
  1893 
  1894 lemma INDEP_BIND: "ALL (f::(nat => bool) => 'a::type * (nat => bool))
  1895    g::'a::type => (nat => bool) => 'b::type * (nat => bool).
  1896    indep f & (ALL x::'a::type. indep (g x)) --> indep (BIND f g)"
  1897   by (import prob_indep INDEP_BIND)
  1898 
  1899 lemma INDEP_PROB: "ALL (f::(nat => bool) => 'a::type * (nat => bool)) (p::'a::type => bool)
  1900    q::(nat => bool) => bool.
  1901    indep f & measurable q -->
  1902    prob (pred_set.INTER (p o (fst o f)) (q o (snd o f))) =
  1903    prob (p o (fst o f)) * prob q"
  1904   by (import prob_indep INDEP_PROB)
  1905 
  1906 lemma INDEP_MEASURABLE1: "ALL (f::(nat => bool) => 'a::type * (nat => bool)) p::'a::type => bool.
  1907    indep f --> measurable (p o (fst o f))"
  1908   by (import prob_indep INDEP_MEASURABLE1)
  1909 
  1910 lemma INDEP_MEASURABLE2: "ALL (f::(nat => bool) => 'a::type * (nat => bool)) q::(nat => bool) => bool.
  1911    indep f & measurable q --> measurable (q o (snd o f))"
  1912   by (import prob_indep INDEP_MEASURABLE2)
  1913 
  1914 lemma PROB_INDEP_BOUND: "ALL (f::(nat => bool) => nat * (nat => bool)) n::nat.
  1915    indep f -->
  1916    prob (%s::nat => bool. fst (f s) < Suc n) =
  1917    prob (%s::nat => bool. fst (f s) < n) +
  1918    prob (%s::nat => bool. fst (f s) = n)"
  1919   by (import prob_indep PROB_INDEP_BOUND)
  1920 
  1921 ;end_setup
  1922 
  1923 ;setup_theory prob_uniform
  1924 
  1925 consts
  1926   unif_bound :: "nat => nat" 
  1927 
  1928 defs
  1929   unif_bound_primdef: "unif_bound ==
  1930 WFREC
  1931  (SOME R::nat => nat => bool. WF R & (ALL v::nat. R (Suc v div 2) (Suc v)))
  1932  (%unif_bound::nat => nat.
  1933      nat_case 0 (%v1::nat. Suc (unif_bound (Suc v1 div 2))))"
  1934 
  1935 lemma unif_bound_primitive_def: "unif_bound =
  1936 WFREC
  1937  (SOME R::nat => nat => bool. WF R & (ALL v::nat. R (Suc v div 2) (Suc v)))
  1938  (%unif_bound::nat => nat.
  1939      nat_case 0 (%v1::nat. Suc (unif_bound (Suc v1 div 2))))"
  1940   by (import prob_uniform unif_bound_primitive_def)
  1941 
  1942 lemma unif_bound_def: "unif_bound 0 = 0 &
  1943 unif_bound (Suc (v::nat)) = Suc (unif_bound (Suc v div 2))"
  1944   by (import prob_uniform unif_bound_def)
  1945 
  1946 lemma unif_bound_ind: "ALL P::nat => bool.
  1947    P 0 & (ALL v::nat. P (Suc v div 2) --> P (Suc v)) --> All P"
  1948   by (import prob_uniform unif_bound_ind)
  1949 
  1950 constdefs
  1951   unif_tupled :: "nat * (nat => bool) => nat * (nat => bool)" 
  1952   "unif_tupled ==
  1953 WFREC
  1954  (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
  1955      WF R & (ALL (s::nat => bool) v2::nat. R (Suc v2 div 2, s) (Suc v2, s)))
  1956  (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
  1957      v1::nat => bool).
  1958      case v of 0 => (0, v1)
  1959      | Suc (v3::nat) =>
  1960          let (m::nat, s'::nat => bool) = unif_tupled (Suc v3 div 2, v1)
  1961          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1962 
  1963 lemma unif_tupled_primitive_def: "unif_tupled =
  1964 WFREC
  1965  (SOME R::nat * (nat => bool) => nat * (nat => bool) => bool.
  1966      WF R & (ALL (s::nat => bool) v2::nat. R (Suc v2 div 2, s) (Suc v2, s)))
  1967  (%(unif_tupled::nat * (nat => bool) => nat * (nat => bool)) (v::nat,
  1968      v1::nat => bool).
  1969      case v of 0 => (0, v1)
  1970      | Suc (v3::nat) =>
  1971          let (m::nat, s'::nat => bool) = unif_tupled (Suc v3 div 2, v1)
  1972          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1973   by (import prob_uniform unif_tupled_primitive_def)
  1974 
  1975 consts
  1976   unif :: "nat => (nat => bool) => nat * (nat => bool)" 
  1977 
  1978 defs
  1979   unif_primdef: "unif == %(x::nat) x1::nat => bool. unif_tupled (x, x1)"
  1980 
  1981 lemma unif_curried_def: "ALL (x::nat) x1::nat => bool. unif x x1 = unif_tupled (x, x1)"
  1982   by (import prob_uniform unif_curried_def)
  1983 
  1984 lemma unif_def: "unif 0 (s::nat => bool) = (0, s) &
  1985 unif (Suc (v2::nat)) s =
  1986 (let (m::nat, s'::nat => bool) = unif (Suc v2 div 2) s
  1987  in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  1988   by (import prob_uniform unif_def)
  1989 
  1990 lemma unif_ind: "ALL P::nat => (nat => bool) => bool.
  1991    All (P 0) &
  1992    (ALL (v2::nat) s::nat => bool. P (Suc v2 div 2) s --> P (Suc v2) s) -->
  1993    (ALL v::nat. All (P v))"
  1994   by (import prob_uniform unif_ind)
  1995 
  1996 constdefs
  1997   uniform_tupled :: "nat * nat * (nat => bool) => nat * (nat => bool)" 
  1998   "uniform_tupled ==
  1999 WFREC
  2000  (SOME R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  2001      WF R &
  2002      (ALL (t::nat) (s::nat => bool) (n::nat) (res::nat) s'::nat => bool.
  2003          (res, s') = unif n s & ~ res < Suc n -->
  2004          R (t, Suc n, s') (Suc t, Suc n, s)))
  2005  (%(uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  2006      (v::nat, v1::nat * (nat => bool)).
  2007      case v of
  2008      0 => (%(v3::nat, v4::nat => bool).
  2009               case v3 of 0 => ARB | Suc (v5::nat) => (0, v4))
  2010            v1
  2011      | Suc (v2::nat) =>
  2012          (%(v7::nat, v8::nat => bool).
  2013              case v7 of 0 => ARB
  2014              | Suc (v9::nat) =>
  2015                  let (res::nat, s'::nat => bool) = unif v9 v8
  2016                  in if res < Suc v9 then (res, s')
  2017                     else uniform_tupled (v2, Suc v9, s'))
  2018           v1)"
  2019 
  2020 lemma uniform_tupled_primitive_def: "uniform_tupled =
  2021 WFREC
  2022  (SOME R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  2023      WF R &
  2024      (ALL (t::nat) (s::nat => bool) (n::nat) (res::nat) s'::nat => bool.
  2025          (res, s') = unif n s & ~ res < Suc n -->
  2026          R (t, Suc n, s') (Suc t, Suc n, s)))
  2027  (%(uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  2028      (v::nat, v1::nat * (nat => bool)).
  2029      case v of
  2030      0 => (%(v3::nat, v4::nat => bool).
  2031               case v3 of 0 => ARB | Suc (v5::nat) => (0, v4))
  2032            v1
  2033      | Suc (v2::nat) =>
  2034          (%(v7::nat, v8::nat => bool).
  2035              case v7 of 0 => ARB
  2036              | Suc (v9::nat) =>
  2037                  let (res::nat, s'::nat => bool) = unif v9 v8
  2038                  in if res < Suc v9 then (res, s')
  2039                     else uniform_tupled (v2, Suc v9, s'))
  2040           v1)"
  2041   by (import prob_uniform uniform_tupled_primitive_def)
  2042 
  2043 consts
  2044   uniform :: "nat => nat => (nat => bool) => nat * (nat => bool)" 
  2045 
  2046 defs
  2047   uniform_primdef: "uniform == %(x::nat) (x1::nat) x2::nat => bool. uniform_tupled (x, x1, x2)"
  2048 
  2049 lemma uniform_curried_def: "ALL (x::nat) (x1::nat) x2::nat => bool.
  2050    uniform x x1 x2 = uniform_tupled (x, x1, x2)"
  2051   by (import prob_uniform uniform_curried_def)
  2052 
  2053 lemma uniform_ind: "ALL P::nat => nat => (nat => bool) => bool.
  2054    (ALL x::nat. All (P (Suc x) 0)) &
  2055    All (P 0 0) &
  2056    (ALL x::nat. All (P 0 (Suc x))) &
  2057    (ALL (x::nat) (xa::nat) xb::nat => bool.
  2058        (ALL (xc::nat) xd::nat => bool.
  2059            (xc, xd) = unif xa xb & ~ xc < Suc xa --> P x (Suc xa) xd) -->
  2060        P (Suc x) (Suc xa) xb) -->
  2061    (ALL (x::nat) xa::nat. All (P x xa))"
  2062   by (import prob_uniform uniform_ind)
  2063 
  2064 lemma uniform_def: "uniform 0 (Suc (n::nat)) (s::nat => bool) = (0, s) &
  2065 uniform (Suc (t::nat)) (Suc n) s =
  2066 (let (xa::nat, x::nat => bool) = unif n s
  2067  in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
  2068   by (import prob_uniform uniform_def)
  2069 
  2070 lemma SUC_DIV_TWO_ZERO: "ALL n::nat. (Suc n div 2 = 0) = (n = 0)"
  2071   by (import prob_uniform SUC_DIV_TWO_ZERO)
  2072 
  2073 lemma UNIF_BOUND_LOWER: "ALL n::nat. n < 2 ^ unif_bound n"
  2074   by (import prob_uniform UNIF_BOUND_LOWER)
  2075 
  2076 lemma UNIF_BOUND_LOWER_SUC: "ALL n::nat. Suc n <= 2 ^ unif_bound n"
  2077   by (import prob_uniform UNIF_BOUND_LOWER_SUC)
  2078 
  2079 lemma UNIF_BOUND_UPPER: "ALL n::nat. n ~= 0 --> 2 ^ unif_bound n <= 2 * n"
  2080   by (import prob_uniform UNIF_BOUND_UPPER)
  2081 
  2082 lemma UNIF_BOUND_UPPER_SUC: "ALL n::nat. 2 ^ unif_bound n <= Suc (2 * n)"
  2083   by (import prob_uniform UNIF_BOUND_UPPER_SUC)
  2084 
  2085 lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
  2086 (ALL n::nat.
  2087     unif (Suc n) =
  2088     BIND (unif (Suc n div 2))
  2089      (%m::nat.
  2090          BIND SDEST (%b::bool. UNIT (if b then 2 * m + 1 else 2 * m))))"
  2091   by (import prob_uniform UNIF_DEF_MONAD)
  2092 
  2093 lemma UNIFORM_DEF_MONAD: "(ALL x::nat. uniform 0 (Suc x) = UNIT 0) &
  2094 (ALL (x::nat) xa::nat.
  2095     uniform (Suc x) (Suc xa) =
  2096     BIND (unif xa)
  2097      (%m::nat. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
  2098   by (import prob_uniform UNIFORM_DEF_MONAD)
  2099 
  2100 lemma INDEP_UNIF: "ALL n::nat. indep (unif n)"
  2101   by (import prob_uniform INDEP_UNIF)
  2102 
  2103 lemma INDEP_UNIFORM: "ALL (t::nat) n::nat. indep (uniform t (Suc n))"
  2104   by (import prob_uniform INDEP_UNIFORM)
  2105 
  2106 lemma PROB_UNIF: "ALL (n::nat) k::nat.
  2107    prob (%s::nat => bool. fst (unif n s) = k) =
  2108    (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
  2109   by (import prob_uniform PROB_UNIF)
  2110 
  2111 lemma UNIF_RANGE: "ALL (n::nat) s::nat => bool. fst (unif n s) < 2 ^ unif_bound n"
  2112   by (import prob_uniform UNIF_RANGE)
  2113 
  2114 lemma PROB_UNIF_PAIR: "ALL (n::nat) (k::nat) k'::nat.
  2115    (prob (%s::nat => bool. fst (unif n s) = k) =
  2116     prob (%s::nat => bool. fst (unif n s) = k')) =
  2117    ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
  2118   by (import prob_uniform PROB_UNIF_PAIR)
  2119 
  2120 lemma PROB_UNIF_BOUND: "ALL (n::nat) k::nat.
  2121    k <= 2 ^ unif_bound n -->
  2122    prob (%s::nat => bool. fst (unif n s) < k) =
  2123    real k * (1 / 2) ^ unif_bound n"
  2124   by (import prob_uniform PROB_UNIF_BOUND)
  2125 
  2126 lemma PROB_UNIF_GOOD: "ALL n::nat. 1 / 2 <= prob (%s::nat => bool. fst (unif n s) < Suc n)"
  2127   by (import prob_uniform PROB_UNIF_GOOD)
  2128 
  2129 lemma UNIFORM_RANGE: "ALL (t::nat) (n::nat) s::nat => bool. fst (uniform t (Suc n) s) < Suc n"
  2130   by (import prob_uniform UNIFORM_RANGE)
  2131 
  2132 lemma PROB_UNIFORM_LOWER_BOUND: "(All::(real => bool) => bool)
  2133  (%b::real.
  2134      (op -->::bool => bool => bool)
  2135       ((All::(nat => bool) => bool)
  2136         (%k::nat.
  2137             (op -->::bool => bool => bool)
  2138              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  2139              ((op <::real => real => bool)
  2140                ((prob::((nat => bool) => bool) => real)
  2141                  (%s::nat => bool.
  2142                      (op =::nat => nat => bool)
  2143                       ((fst::nat * (nat => bool) => nat)
  2144                         ((uniform::nat
  2145                                    => nat
  2146 => (nat => bool) => nat * (nat => bool))
  2147                           (t::nat) ((Suc::nat => nat) n) s))
  2148                       k))
  2149                b)))
  2150       ((All::(nat => bool) => bool)
  2151         (%m::nat.
  2152             (op -->::bool => bool => bool)
  2153              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  2154              ((op <::real => real => bool)
  2155                ((prob::((nat => bool) => bool) => real)
  2156                  (%s::nat => bool.
  2157                      (op <::nat => nat => bool)
  2158                       ((fst::nat * (nat => bool) => nat)
  2159                         ((uniform::nat
  2160                                    => nat
  2161 => (nat => bool) => nat * (nat => bool))
  2162                           t ((Suc::nat => nat) n) s))
  2163                       ((Suc::nat => nat) m)))
  2164                ((op *::real => real => real)
  2165                  ((real::nat => real) ((Suc::nat => nat) m)) b)))))"
  2166   by (import prob_uniform PROB_UNIFORM_LOWER_BOUND)
  2167 
  2168 lemma PROB_UNIFORM_UPPER_BOUND: "(All::(real => bool) => bool)
  2169  (%b::real.
  2170      (op -->::bool => bool => bool)
  2171       ((All::(nat => bool) => bool)
  2172         (%k::nat.
  2173             (op -->::bool => bool => bool)
  2174              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  2175              ((op <::real => real => bool) b
  2176                ((prob::((nat => bool) => bool) => real)
  2177                  (%s::nat => bool.
  2178                      (op =::nat => nat => bool)
  2179                       ((fst::nat * (nat => bool) => nat)
  2180                         ((uniform::nat
  2181                                    => nat
  2182 => (nat => bool) => nat * (nat => bool))
  2183                           (t::nat) ((Suc::nat => nat) n) s))
  2184                       k)))))
  2185       ((All::(nat => bool) => bool)
  2186         (%m::nat.
  2187             (op -->::bool => bool => bool)
  2188              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  2189              ((op <::real => real => bool)
  2190                ((op *::real => real => real)
  2191                  ((real::nat => real) ((Suc::nat => nat) m)) b)
  2192                ((prob::((nat => bool) => bool) => real)
  2193                  (%s::nat => bool.
  2194                      (op <::nat => nat => bool)
  2195                       ((fst::nat * (nat => bool) => nat)
  2196                         ((uniform::nat
  2197                                    => nat
  2198 => (nat => bool) => nat * (nat => bool))
  2199                           t ((Suc::nat => nat) n) s))
  2200                       ((Suc::nat => nat) m)))))))"
  2201   by (import prob_uniform PROB_UNIFORM_UPPER_BOUND)
  2202 
  2203 lemma PROB_UNIFORM_PAIR_SUC: "ALL (t::nat) (n::nat) (k::nat) k'::nat.
  2204    k < Suc n & k' < Suc n -->
  2205    abs (prob (%s::nat => bool. fst (uniform t (Suc n) s) = k) -
  2206         prob (%s::nat => bool. fst (uniform t (Suc n) s) = k'))
  2207    <= (1 / 2) ^ t"
  2208   by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
  2209 
  2210 lemma PROB_UNIFORM_SUC: "ALL (t::nat) (n::nat) k::nat.
  2211    k < Suc n -->
  2212    abs (prob (%s::nat => bool. fst (uniform t (Suc n) s) = k) -
  2213         1 / real (Suc n))
  2214    <= (1 / 2) ^ t"
  2215   by (import prob_uniform PROB_UNIFORM_SUC)
  2216 
  2217 lemma PROB_UNIFORM: "ALL (t::nat) (n::nat) k::nat.
  2218    k < n -->
  2219    abs (prob (%s::nat => bool. fst (uniform t n s) = k) - 1 / real n)
  2220    <= (1 / 2) ^ t"
  2221   by (import prob_uniform PROB_UNIFORM)
  2222 
  2223 ;end_setup
  2224 
  2225 end
  2226