src/HOL/Import/HOL/HOL4Prob.thy
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14516 a183dec876ab
child 15071 b65fc0787fbe
permissions -rw-r--r--
new treatment of binary numerals
     1 theory HOL4Prob = HOL4Real:
     2 
     3 ;setup_theory prob_extra
     4 
     5 lemma BOOL_BOOL_CASES_THM: "ALL f. f = (%b. False) | f = (%b. True) | f = (%b. b) | f = Not"
     6   by (import prob_extra BOOL_BOOL_CASES_THM)
     7 
     8 lemma EVEN_ODD_BASIC: "EVEN 0 & ~ EVEN 1 & EVEN 2 & ~ ODD 0 & ODD 1 & ~ ODD 2"
     9   by (import prob_extra EVEN_ODD_BASIC)
    10 
    11 lemma EVEN_ODD_EXISTS_EQ: "ALL n. EVEN n = (EX m. n = 2 * m) & ODD n = (EX m. n = Suc (2 * m))"
    12   by (import prob_extra EVEN_ODD_EXISTS_EQ)
    13 
    14 lemma DIV_THEN_MULT: "ALL p q. Suc q * (p div Suc q) <= p"
    15   by (import prob_extra DIV_THEN_MULT)
    16 
    17 lemma DIV_TWO_UNIQUE: "(All::(nat => bool) => bool)
    18  (%n::nat.
    19      (All::(nat => bool) => bool)
    20       (%q::nat.
    21           (All::(nat => bool) => bool)
    22            (%r::nat.
    23                (op -->::bool => bool => bool)
    24                 ((op &::bool => bool => bool)
    25                   ((op =::nat => nat => bool) n
    26                     ((op +::nat => nat => nat)
    27                       ((op *::nat => nat => nat)
    28                         ((number_of::bin => nat)
    29                           ((op BIT::bin => bool => bin)
    30                             ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    31                               (True::bool))
    32                             (False::bool)))
    33                         q)
    34                       r))
    35                   ((op |::bool => bool => bool)
    36                     ((op =::nat => nat => bool) r (0::nat))
    37                     ((op =::nat => nat => bool) r (1::nat))))
    38                 ((op &::bool => bool => bool)
    39                   ((op =::nat => nat => bool) q
    40                     ((op div::nat => nat => nat) n
    41                       ((number_of::bin => nat)
    42                         ((op BIT::bin => bool => bin)
    43                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    44                             (True::bool))
    45                           (False::bool)))))
    46                   ((op =::nat => nat => bool) r
    47                     ((op mod::nat => nat => nat) n
    48                       ((number_of::bin => nat)
    49                         ((op BIT::bin => bool => bin)
    50                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    51                             (True::bool))
    52                           (False::bool)))))))))"
    53   by (import prob_extra DIV_TWO_UNIQUE)
    54 
    55 lemma DIVISION_TWO: "ALL n::nat.
    56    n = (2::nat) * (n div (2::nat)) + n mod (2::nat) &
    57    (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))"
    58   by (import prob_extra DIVISION_TWO)
    59 
    60 lemma DIV_TWO: "ALL n::nat. n = (2::nat) * (n div (2::nat)) + n mod (2::nat)"
    61   by (import prob_extra DIV_TWO)
    62 
    63 lemma MOD_TWO: "ALL n. n mod 2 = (if EVEN n then 0 else 1)"
    64   by (import prob_extra MOD_TWO)
    65 
    66 lemma DIV_TWO_BASIC: "(0::nat) div (2::nat) = (0::nat) &
    67 (1::nat) div (2::nat) = (0::nat) & (2::nat) div (2::nat) = (1::nat)"
    68   by (import prob_extra DIV_TWO_BASIC)
    69 
    70 lemma DIV_TWO_MONO: "(All::(nat => bool) => bool)
    71  (%m::nat.
    72      (All::(nat => bool) => bool)
    73       (%n::nat.
    74           (op -->::bool => bool => bool)
    75            ((op <::nat => nat => bool)
    76              ((op div::nat => nat => nat) m
    77                ((number_of::bin => nat)
    78                  ((op BIT::bin => bool => bin)
    79                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    80                      (True::bool))
    81                    (False::bool))))
    82              ((op div::nat => nat => nat) n
    83                ((number_of::bin => nat)
    84                  ((op BIT::bin => bool => bin)
    85                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
    86                      (True::bool))
    87                    (False::bool)))))
    88            ((op <::nat => nat => bool) m n)))"
    89   by (import prob_extra DIV_TWO_MONO)
    90 
    91 lemma DIV_TWO_MONO_EVEN: "(All::(nat => bool) => bool)
    92  (%m::nat.
    93      (All::(nat => bool) => bool)
    94       (%n::nat.
    95           (op -->::bool => bool => bool) ((EVEN::nat => bool) n)
    96            ((op =::bool => bool => bool)
    97              ((op <::nat => nat => bool)
    98                ((op div::nat => nat => nat) m
    99                  ((number_of::bin => nat)
   100                    ((op BIT::bin => bool => bin)
   101                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   102                        (True::bool))
   103                      (False::bool))))
   104                ((op div::nat => nat => nat) n
   105                  ((number_of::bin => nat)
   106                    ((op BIT::bin => bool => bin)
   107                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   108                        (True::bool))
   109                      (False::bool)))))
   110              ((op <::nat => nat => bool) m n))))"
   111   by (import prob_extra DIV_TWO_MONO_EVEN)
   112 
   113 lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n"
   114   by (import prob_extra DIV_TWO_CANCEL)
   115 
   116 lemma EXP_DIV_TWO: "ALL n::nat. (2::nat) ^ Suc n div (2::nat) = (2::nat) ^ n"
   117   by (import prob_extra EXP_DIV_TWO)
   118 
   119 lemma EVEN_EXP_TWO: "ALL n. EVEN (2 ^ n) = (n ~= 0)"
   120   by (import prob_extra EVEN_EXP_TWO)
   121 
   122 lemma DIV_TWO_EXP: "ALL (n::nat) k::nat.
   123    (k div (2::nat) < (2::nat) ^ n) = (k < (2::nat) ^ Suc n)"
   124   by (import prob_extra DIV_TWO_EXP)
   125 
   126 consts
   127   inf :: "(real => bool) => real" 
   128 
   129 defs
   130   inf_primdef: "inf == %P. - sup (IMAGE uminus P)"
   131 
   132 lemma inf_def: "ALL P. inf P = - sup (IMAGE uminus P)"
   133   by (import prob_extra inf_def)
   134 
   135 lemma INF_DEF_ALT: "ALL P. inf P = - sup (%r. P (- r))"
   136   by (import prob_extra INF_DEF_ALT)
   137 
   138 lemma REAL_SUP_EXISTS_UNIQUE: "(All::((real => bool) => bool) => bool)
   139  (%P::real => bool.
   140      (op -->::bool => bool => bool)
   141       ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   142         ((Ex::(real => bool) => bool)
   143           (%z::real.
   144               (All::(real => bool) => bool)
   145                (%x::real.
   146                    (op -->::bool => bool => bool) (P x)
   147                     ((op <=::real => real => bool) x z)))))
   148       ((Ex1::(real => bool) => bool)
   149         (%s::real.
   150             (All::(real => bool) => bool)
   151              (%y::real.
   152                  (op =::bool => bool => bool)
   153                   ((Ex::(real => bool) => bool)
   154                     (%x::real.
   155                         (op &::bool => bool => bool) (P x)
   156                          ((op <::real => real => bool) y x)))
   157                   ((op <::real => real => bool) y s)))))"
   158   by (import prob_extra REAL_SUP_EXISTS_UNIQUE)
   159 
   160 lemma REAL_SUP_MAX: "(All::((real => bool) => bool) => bool)
   161  (%P::real => bool.
   162      (All::(real => bool) => bool)
   163       (%z::real.
   164           (op -->::bool => bool => bool)
   165            ((op &::bool => bool => bool) (P z)
   166              ((All::(real => bool) => bool)
   167                (%x::real.
   168                    (op -->::bool => bool => bool) (P x)
   169                     ((op <=::real => real => bool) x z))))
   170            ((op =::real => real => bool) ((sup::(real => bool) => real) P)
   171              z)))"
   172   by (import prob_extra REAL_SUP_MAX)
   173 
   174 lemma REAL_INF_MIN: "(All::((real => bool) => bool) => bool)
   175  (%P::real => bool.
   176      (All::(real => bool) => bool)
   177       (%z::real.
   178           (op -->::bool => bool => bool)
   179            ((op &::bool => bool => bool) (P z)
   180              ((All::(real => bool) => bool)
   181                (%x::real.
   182                    (op -->::bool => bool => bool) (P x)
   183                     ((op <=::real => real => bool) z x))))
   184            ((op =::real => real => bool) ((inf::(real => bool) => real) P)
   185              z)))"
   186   by (import prob_extra REAL_INF_MIN)
   187 
   188 lemma HALF_POS: "(0::real) < (1::real) / (2::real)"
   189   by (import prob_extra HALF_POS)
   190 
   191 lemma HALF_CANCEL: "(2::real) * ((1::real) / (2::real)) = (1::real)"
   192   by (import prob_extra HALF_CANCEL)
   193 
   194 lemma POW_HALF_POS: "ALL n::nat. (0::real) < ((1::real) / (2::real)) ^ n"
   195   by (import prob_extra POW_HALF_POS)
   196 
   197 lemma POW_HALF_MONO: "(All::(nat => bool) => bool)
   198  (%m::nat.
   199      (All::(nat => bool) => bool)
   200       (%n::nat.
   201           (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n)
   202            ((op <=::real => real => bool)
   203              ((op ^::real => nat => real)
   204                ((op /::real => real => real) (1::real)
   205                  ((number_of::bin => real)
   206                    ((op BIT::bin => bool => bin)
   207                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   208                        (True::bool))
   209                      (False::bool))))
   210                n)
   211              ((op ^::real => nat => real)
   212                ((op /::real => real => real) (1::real)
   213                  ((number_of::bin => real)
   214                    ((op BIT::bin => bool => bin)
   215                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
   216                        (True::bool))
   217                      (False::bool))))
   218                m))))"
   219   by (import prob_extra POW_HALF_MONO)
   220 
   221 lemma POW_HALF_TWICE: "ALL n::nat.
   222    ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n"
   223   by (import prob_extra POW_HALF_TWICE)
   224 
   225 lemma X_HALF_HALF: "ALL x::real. (1::real) / (2::real) * x + (1::real) / (2::real) * x = x"
   226   by (import prob_extra X_HALF_HALF)
   227 
   228 lemma REAL_SUP_LE_X: "(All::((real => bool) => bool) => bool)
   229  (%P::real => bool.
   230      (All::(real => bool) => bool)
   231       (%x::real.
   232           (op -->::bool => bool => bool)
   233            ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   234              ((All::(real => bool) => bool)
   235                (%r::real.
   236                    (op -->::bool => bool => bool) (P r)
   237                     ((op <=::real => real => bool) r x))))
   238            ((op <=::real => real => bool) ((sup::(real => bool) => real) P)
   239              x)))"
   240   by (import prob_extra REAL_SUP_LE_X)
   241 
   242 lemma REAL_X_LE_SUP: "(All::((real => bool) => bool) => bool)
   243  (%P::real => bool.
   244      (All::(real => bool) => bool)
   245       (%x::real.
   246           (op -->::bool => bool => bool)
   247            ((op &::bool => bool => bool) ((Ex::(real => bool) => bool) P)
   248              ((op &::bool => bool => bool)
   249                ((Ex::(real => bool) => bool)
   250                  (%z::real.
   251                      (All::(real => bool) => bool)
   252                       (%r::real.
   253                           (op -->::bool => bool => bool) (P r)
   254                            ((op <=::real => real => bool) r z))))
   255                ((Ex::(real => bool) => bool)
   256                  (%r::real.
   257                      (op &::bool => bool => bool) (P r)
   258                       ((op <=::real => real => bool) x r)))))
   259            ((op <=::real => real => bool) x
   260              ((sup::(real => bool) => real) P))))"
   261   by (import prob_extra REAL_X_LE_SUP)
   262 
   263 lemma ABS_BETWEEN_LE: "ALL (x::real) (y::real) d::real.
   264    ((0::real) <= d & x - d <= y & y <= x + d) = (abs (y - x) <= d)"
   265   by (import prob_extra ABS_BETWEEN_LE)
   266 
   267 lemma ONE_MINUS_HALF: "(1::real) - (1::real) / (2::real) = (1::real) / (2::real)"
   268   by (import prob_extra ONE_MINUS_HALF)
   269 
   270 lemma HALF_LT_1: "(1::real) / (2::real) < (1::real)"
   271   by (import prob_extra HALF_LT_1)
   272 
   273 lemma POW_HALF_EXP: "ALL n::nat. ((1::real) / (2::real)) ^ n = inverse (real ((2::nat) ^ n))"
   274   by (import prob_extra POW_HALF_EXP)
   275 
   276 lemma INV_SUC_POS: "ALL n. 0 < 1 / real (Suc n)"
   277   by (import prob_extra INV_SUC_POS)
   278 
   279 lemma INV_SUC_MAX: "ALL x. 1 / real (Suc x) <= 1"
   280   by (import prob_extra INV_SUC_MAX)
   281 
   282 lemma INV_SUC: "ALL n. 0 < 1 / real (Suc n) & 1 / real (Suc n) <= 1"
   283   by (import prob_extra INV_SUC)
   284 
   285 lemma ABS_UNIT_INTERVAL: "(All::(real => bool) => bool)
   286  (%x::real.
   287      (All::(real => bool) => bool)
   288       (%y::real.
   289           (op -->::bool => bool => bool)
   290            ((op &::bool => bool => bool)
   291              ((op <=::real => real => bool) (0::real) x)
   292              ((op &::bool => bool => bool)
   293                ((op <=::real => real => bool) x (1::real))
   294                ((op &::bool => bool => bool)
   295                  ((op <=::real => real => bool) (0::real) y)
   296                  ((op <=::real => real => bool) y (1::real)))))
   297            ((op <=::real => real => bool)
   298              ((abs::real => real) ((op -::real => real => real) x y))
   299              (1::real))))"
   300   by (import prob_extra ABS_UNIT_INTERVAL)
   301 
   302 lemma MEM_NIL: "ALL l. (ALL x. ~ x mem l) = (l = [])"
   303   by (import prob_extra MEM_NIL)
   304 
   305 lemma MAP_MEM: "ALL f l x. x mem map f l = (EX y. y mem l & x = f y)"
   306   by (import prob_extra MAP_MEM)
   307 
   308 lemma MEM_NIL_MAP_CONS: "ALL x l. ~ [] mem map (op # x) l"
   309   by (import prob_extra MEM_NIL_MAP_CONS)
   310 
   311 lemma FILTER_TRUE: "ALL l. [x:l. True] = l"
   312   by (import prob_extra FILTER_TRUE)
   313 
   314 lemma FILTER_FALSE: "ALL l. [x:l. False] = []"
   315   by (import prob_extra FILTER_FALSE)
   316 
   317 lemma FILTER_MEM: "(All::(('a => bool) => bool) => bool)
   318  (%P::'a => bool.
   319      (All::('a => bool) => bool)
   320       (%x::'a.
   321           (All::('a list => bool) => bool)
   322            (%l::'a list.
   323                (op -->::bool => bool => bool)
   324                 ((op mem::'a => 'a list => bool) x
   325                   ((filter::('a => bool) => 'a list => 'a list) P l))
   326                 (P x))))"
   327   by (import prob_extra FILTER_MEM)
   328 
   329 lemma MEM_FILTER: "(All::(('a => bool) => bool) => bool)
   330  (%P::'a => bool.
   331      (All::('a list => bool) => bool)
   332       (%l::'a list.
   333           (All::('a => bool) => bool)
   334            (%x::'a.
   335                (op -->::bool => bool => bool)
   336                 ((op mem::'a => 'a list => bool) x
   337                   ((filter::('a => bool) => 'a list => 'a list) P l))
   338                 ((op mem::'a => 'a list => bool) x l))))"
   339   by (import prob_extra MEM_FILTER)
   340 
   341 lemma FILTER_OUT_ELT: "ALL x l. x mem l | [y:l. y ~= x] = l"
   342   by (import prob_extra FILTER_OUT_ELT)
   343 
   344 lemma IS_PREFIX_NIL: "ALL x. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
   345   by (import prob_extra IS_PREFIX_NIL)
   346 
   347 lemma IS_PREFIX_REFL: "ALL x. IS_PREFIX x x"
   348   by (import prob_extra IS_PREFIX_REFL)
   349 
   350 lemma IS_PREFIX_ANTISYM: "(All::('a list => bool) => bool)
   351  (%x::'a list.
   352      (All::('a list => bool) => bool)
   353       (%y::'a list.
   354           (op -->::bool => bool => bool)
   355            ((op &::bool => bool => bool)
   356              ((IS_PREFIX::'a list => 'a list => bool) y x)
   357              ((IS_PREFIX::'a list => 'a list => bool) x y))
   358            ((op =::'a list => 'a list => bool) x y)))"
   359   by (import prob_extra IS_PREFIX_ANTISYM)
   360 
   361 lemma IS_PREFIX_TRANS: "(All::('a list => bool) => bool)
   362  (%x::'a list.
   363      (All::('a list => bool) => bool)
   364       (%y::'a list.
   365           (All::('a list => bool) => bool)
   366            (%z::'a list.
   367                (op -->::bool => bool => bool)
   368                 ((op &::bool => bool => bool)
   369                   ((IS_PREFIX::'a list => 'a list => bool) x y)
   370                   ((IS_PREFIX::'a list => 'a list => bool) y z))
   371                 ((IS_PREFIX::'a list => 'a list => bool) x z))))"
   372   by (import prob_extra IS_PREFIX_TRANS)
   373 
   374 lemma IS_PREFIX_BUTLAST: "ALL x y. IS_PREFIX (x # y) (butlast (x # y))"
   375   by (import prob_extra IS_PREFIX_BUTLAST)
   376 
   377 lemma IS_PREFIX_LENGTH: "(All::('a list => bool) => bool)
   378  (%x::'a list.
   379      (All::('a list => bool) => bool)
   380       (%y::'a list.
   381           (op -->::bool => bool => bool)
   382            ((IS_PREFIX::'a list => 'a list => bool) y x)
   383            ((op <=::nat => nat => bool) ((size::'a list => nat) x)
   384              ((size::'a list => nat) y))))"
   385   by (import prob_extra IS_PREFIX_LENGTH)
   386 
   387 lemma IS_PREFIX_LENGTH_ANTI: "(All::('a list => bool) => bool)
   388  (%x::'a list.
   389      (All::('a list => bool) => bool)
   390       (%y::'a list.
   391           (op -->::bool => bool => bool)
   392            ((op &::bool => bool => bool)
   393              ((IS_PREFIX::'a list => 'a list => bool) y x)
   394              ((op =::nat => nat => bool) ((size::'a list => nat) x)
   395                ((size::'a list => nat) y)))
   396            ((op =::'a list => 'a list => bool) x y)))"
   397   by (import prob_extra IS_PREFIX_LENGTH_ANTI)
   398 
   399 lemma IS_PREFIX_SNOC: "ALL x y z. IS_PREFIX (SNOC x y) z = (IS_PREFIX y z | z = SNOC x y)"
   400   by (import prob_extra IS_PREFIX_SNOC)
   401 
   402 lemma FOLDR_MAP: "ALL (f::'b => 'c => 'c) (e::'c) (g::'a => 'b) l::'a list.
   403    foldr f (map g l) e = foldr (%x::'a. f (g x)) l e"
   404   by (import prob_extra FOLDR_MAP)
   405 
   406 lemma LAST_MEM: "ALL h t. last (h # t) mem h # t"
   407   by (import prob_extra LAST_MEM)
   408 
   409 lemma LAST_MAP_CONS: "ALL (b::bool) (h::bool list) t::bool list list.
   410    EX x::bool list. last (map (op # b) (h # t)) = b # x"
   411   by (import prob_extra LAST_MAP_CONS)
   412 
   413 lemma EXISTS_LONGEST: "(All::('a list => bool) => bool)
   414  (%x::'a list.
   415      (All::('a list list => bool) => bool)
   416       (%y::'a list list.
   417           (Ex::('a list => bool) => bool)
   418            (%z::'a list.
   419                (op &::bool => bool => bool)
   420                 ((op mem::'a list => 'a list list => bool) z
   421                   ((op #::'a list => 'a list list => 'a list list) x y))
   422                 ((All::('a list => bool) => bool)
   423                   (%w::'a list.
   424                       (op -->::bool => bool => bool)
   425                        ((op mem::'a list => 'a list list => bool) w
   426                          ((op #::'a list => 'a list list => 'a list list) x
   427                            y))
   428                        ((op <=::nat => nat => bool)
   429                          ((size::'a list => nat) w)
   430                          ((size::'a list => nat) z)))))))"
   431   by (import prob_extra EXISTS_LONGEST)
   432 
   433 lemma UNION_DEF_ALT: "ALL s t. pred_set.UNION s t = (%x. s x | t x)"
   434   by (import prob_extra UNION_DEF_ALT)
   435 
   436 lemma INTER_UNION_RDISTRIB: "ALL p q r.
   437    pred_set.INTER (pred_set.UNION p q) r =
   438    pred_set.UNION (pred_set.INTER p r) (pred_set.INTER q r)"
   439   by (import prob_extra INTER_UNION_RDISTRIB)
   440 
   441 lemma SUBSET_EQ: "ALL x xa. (x = xa) = (SUBSET x xa & SUBSET xa x)"
   442   by (import prob_extra SUBSET_EQ)
   443 
   444 lemma INTER_IS_EMPTY: "ALL s t. (pred_set.INTER s t = EMPTY) = (ALL x. ~ s x | ~ t x)"
   445   by (import prob_extra INTER_IS_EMPTY)
   446 
   447 lemma UNION_DISJOINT_SPLIT: "(All::(('a => bool) => bool) => bool)
   448  (%s::'a => bool.
   449      (All::(('a => bool) => bool) => bool)
   450       (%t::'a => bool.
   451           (All::(('a => bool) => bool) => bool)
   452            (%u::'a => bool.
   453                (op -->::bool => bool => bool)
   454                 ((op &::bool => bool => bool)
   455                   ((op =::('a => bool) => ('a => bool) => bool)
   456                     ((pred_set.UNION::('a => bool)
   457 => ('a => bool) => 'a => bool)
   458                       s t)
   459                     ((pred_set.UNION::('a => bool)
   460 => ('a => bool) => 'a => bool)
   461                       s u))
   462                   ((op &::bool => bool => bool)
   463                     ((op =::('a => bool) => ('a => bool) => bool)
   464                       ((pred_set.INTER::('a => bool)
   465   => ('a => bool) => 'a => bool)
   466                         s t)
   467                       (EMPTY::'a => bool))
   468                     ((op =::('a => bool) => ('a => bool) => bool)
   469                       ((pred_set.INTER::('a => bool)
   470   => ('a => bool) => 'a => bool)
   471                         s u)
   472                       (EMPTY::'a => bool))))
   473                 ((op =::('a => bool) => ('a => bool) => bool) t u))))"
   474   by (import prob_extra UNION_DISJOINT_SPLIT)
   475 
   476 lemma GSPEC_DEF_ALT: "ALL f. GSPEC f = (%v. EX x. (v, True) = f x)"
   477   by (import prob_extra GSPEC_DEF_ALT)
   478 
   479 ;end_setup
   480 
   481 ;setup_theory prob_canon
   482 
   483 consts
   484   alg_twin :: "bool list => bool list => bool" 
   485 
   486 defs
   487   alg_twin_primdef: "alg_twin == %x y. EX l. x = SNOC True l & y = SNOC False l"
   488 
   489 lemma alg_twin_def: "ALL x y. alg_twin x y = (EX l. x = SNOC True l & y = SNOC False l)"
   490   by (import prob_canon alg_twin_def)
   491 
   492 constdefs
   493   alg_order_tupled :: "bool list * bool list => bool" 
   494   "(op ==::(bool list * bool list => bool)
   495         => (bool list * bool list => bool) => prop)
   496  (alg_order_tupled::bool list * bool list => bool)
   497  ((WFREC::(bool list * bool list => bool list * bool list => bool)
   498           => ((bool list * bool list => bool)
   499               => bool list * bool list => bool)
   500              => bool list * bool list => bool)
   501    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   502           => bool list * bool list => bool list * bool list => bool)
   503      (%R::bool list * bool list => bool list * bool list => bool.
   504          (op &::bool => bool => bool)
   505           ((WF::(bool list * bool list => bool list * bool list => bool)
   506                 => bool)
   507             R)
   508           ((All::(bool => bool) => bool)
   509             (%h'::bool.
   510                 (All::(bool => bool) => bool)
   511                  (%h::bool.
   512                      (All::(bool list => bool) => bool)
   513                       (%t'::bool list.
   514                           (All::(bool list => bool) => bool)
   515                            (%t::bool list.
   516                                R ((Pair::bool list
   517    => bool list => bool list * bool list)
   518                                    t t')
   519                                 ((Pair::bool list
   520   => bool list => bool list * bool list)
   521                                   ((op #::bool => bool list => bool list) h
   522                                     t)
   523                                   ((op #::bool => bool list => bool list) h'
   524                                     t')))))))))
   525    (%alg_order_tupled::bool list * bool list => bool.
   526        (split::(bool list => bool list => bool)
   527                => bool list * bool list => bool)
   528         (%(v::bool list) v1::bool list.
   529             (list_case::bool
   530                         => (bool => bool list => bool) => bool list => bool)
   531              ((list_case::bool
   532                           => (bool => bool list => bool)
   533                              => bool list => bool)
   534                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   535              (%(v4::bool) v5::bool list.
   536                  (list_case::bool
   537                              => (bool => bool list => bool)
   538                                 => bool list => bool)
   539                   (False::bool)
   540                   (%(v10::bool) v11::bool list.
   541                       (op |::bool => bool => bool)
   542                        ((op &::bool => bool => bool)
   543                          ((op =::bool => bool => bool) v4 (True::bool))
   544                          ((op =::bool => bool => bool) v10 (False::bool)))
   545                        ((op &::bool => bool => bool)
   546                          ((op =::bool => bool => bool) v4 v10)
   547                          (alg_order_tupled
   548                            ((Pair::bool list
   549                                    => bool list => bool list * bool list)
   550                              v5 v11))))
   551                   v1)
   552              v)))"
   553 
   554 lemma alg_order_tupled_primitive_def: "(op =::(bool list * bool list => bool)
   555        => (bool list * bool list => bool) => bool)
   556  (alg_order_tupled::bool list * bool list => bool)
   557  ((WFREC::(bool list * bool list => bool list * bool list => bool)
   558           => ((bool list * bool list => bool)
   559               => bool list * bool list => bool)
   560              => bool list * bool list => bool)
   561    ((Eps::((bool list * bool list => bool list * bool list => bool) => bool)
   562           => bool list * bool list => bool list * bool list => bool)
   563      (%R::bool list * bool list => bool list * bool list => bool.
   564          (op &::bool => bool => bool)
   565           ((WF::(bool list * bool list => bool list * bool list => bool)
   566                 => bool)
   567             R)
   568           ((All::(bool => bool) => bool)
   569             (%h'::bool.
   570                 (All::(bool => bool) => bool)
   571                  (%h::bool.
   572                      (All::(bool list => bool) => bool)
   573                       (%t'::bool list.
   574                           (All::(bool list => bool) => bool)
   575                            (%t::bool list.
   576                                R ((Pair::bool list
   577    => bool list => bool list * bool list)
   578                                    t t')
   579                                 ((Pair::bool list
   580   => bool list => bool list * bool list)
   581                                   ((op #::bool => bool list => bool list) h
   582                                     t)
   583                                   ((op #::bool => bool list => bool list) h'
   584                                     t')))))))))
   585    (%alg_order_tupled::bool list * bool list => bool.
   586        (split::(bool list => bool list => bool)
   587                => bool list * bool list => bool)
   588         (%(v::bool list) v1::bool list.
   589             (list_case::bool
   590                         => (bool => bool list => bool) => bool list => bool)
   591              ((list_case::bool
   592                           => (bool => bool list => bool)
   593                              => bool list => bool)
   594                (True::bool) (%(v8::bool) v9::bool list. True::bool) v1)
   595              (%(v4::bool) v5::bool list.
   596                  (list_case::bool
   597                              => (bool => bool list => bool)
   598                                 => bool list => bool)
   599                   (False::bool)
   600                   (%(v10::bool) v11::bool list.
   601                       (op |::bool => bool => bool)
   602                        ((op &::bool => bool => bool)
   603                          ((op =::bool => bool => bool) v4 (True::bool))
   604                          ((op =::bool => bool => bool) v10 (False::bool)))
   605                        ((op &::bool => bool => bool)
   606                          ((op =::bool => bool => bool) v4 v10)
   607                          (alg_order_tupled
   608                            ((Pair::bool list
   609                                    => bool list => bool list * bool list)
   610                              v5 v11))))
   611                   v1)
   612              v)))"
   613   by (import prob_canon alg_order_tupled_primitive_def)
   614 
   615 consts
   616   alg_order :: "bool list => bool list => bool" 
   617 
   618 defs
   619   alg_order_primdef: "alg_order == %x x1. alg_order_tupled (x, x1)"
   620 
   621 lemma alg_order_curried_def: "ALL x x1. alg_order x x1 = alg_order_tupled (x, x1)"
   622   by (import prob_canon alg_order_curried_def)
   623 
   624 lemma alg_order_ind: "(All::((bool list => bool list => bool) => bool) => bool)
   625  (%P::bool list => bool list => bool.
   626      (op -->::bool => bool => bool)
   627       ((op &::bool => bool => bool)
   628         ((All::(bool => bool) => bool)
   629           (%x::bool.
   630               (All::(bool list => bool) => bool)
   631                (%xa::bool list.
   632                    P ([]::bool list)
   633                     ((op #::bool => bool list => bool list) x xa))))
   634         ((op &::bool => bool => bool) (P ([]::bool list) ([]::bool list))
   635           ((op &::bool => bool => bool)
   636             ((All::(bool => bool) => bool)
   637               (%x::bool.
   638                   (All::(bool list => bool) => bool)
   639                    (%xa::bool list.
   640                        P ((op #::bool => bool list => bool list) x xa)
   641                         ([]::bool list))))
   642             ((All::(bool => bool) => bool)
   643               (%x::bool.
   644                   (All::(bool list => bool) => bool)
   645                    (%xa::bool list.
   646                        (All::(bool => bool) => bool)
   647                         (%xb::bool.
   648                             (All::(bool list => bool) => bool)
   649                              (%xc::bool list.
   650                                  (op -->::bool => bool => bool) (P xa xc)
   651                                   (P ((op #::bool => bool list => bool list)
   652  x xa)
   653                                     ((op #::bool => bool list => bool list)
   654 xb xc))))))))))
   655       ((All::(bool list => bool) => bool)
   656         (%x::bool list. (All::(bool list => bool) => bool) (P x))))"
   657   by (import prob_canon alg_order_ind)
   658 
   659 lemma alg_order_def: "alg_order [] (v6 # v7) = True &
   660 alg_order [] [] = True &
   661 alg_order (v2 # v3) [] = False &
   662 alg_order (h # t) (h' # t') =
   663 (h = True & h' = False | h = h' & alg_order t t')"
   664   by (import prob_canon alg_order_def)
   665 
   666 consts
   667   alg_sorted :: "bool list list => bool" 
   668 
   669 defs
   670   alg_sorted_primdef: "alg_sorted ==
   671 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   672  (%alg_sorted.
   673      list_case True
   674       (%v2. list_case True
   675              (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
   676 
   677 lemma alg_sorted_primitive_def: "alg_sorted =
   678 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   679  (%alg_sorted.
   680      list_case True
   681       (%v2. list_case True
   682              (%v6 v7. alg_order v2 v6 & alg_sorted (v6 # v7))))"
   683   by (import prob_canon alg_sorted_primitive_def)
   684 
   685 lemma alg_sorted_ind: "(All::((bool list list => bool) => bool) => bool)
   686  (%P::bool list list => bool.
   687      (op -->::bool => bool => bool)
   688       ((op &::bool => bool => bool)
   689         ((All::(bool list => bool) => bool)
   690           (%x::bool list.
   691               (All::(bool list => bool) => bool)
   692                (%y::bool list.
   693                    (All::(bool list list => bool) => bool)
   694                     (%z::bool list list.
   695                         (op -->::bool => bool => bool)
   696                          (P ((op #::bool list
   697                                     => bool list list => bool list list)
   698                               y z))
   699                          (P ((op #::bool list
   700                                     => bool list list => bool list list)
   701                               x ((op #::bool list
   702   => bool list list => bool list list)
   703                                   y z)))))))
   704         ((op &::bool => bool => bool)
   705           ((All::(bool list => bool) => bool)
   706             (%v::bool list.
   707                 P ((op #::bool list => bool list list => bool list list) v
   708                     ([]::bool list list))))
   709           (P ([]::bool list list))))
   710       ((All::(bool list list => bool) => bool) P))"
   711   by (import prob_canon alg_sorted_ind)
   712 
   713 lemma alg_sorted_def: "alg_sorted (x # y # z) = (alg_order x y & alg_sorted (y # z)) &
   714 alg_sorted [v] = True & alg_sorted [] = True"
   715   by (import prob_canon alg_sorted_def)
   716 
   717 consts
   718   alg_prefixfree :: "bool list list => bool" 
   719 
   720 defs
   721   alg_prefixfree_primdef: "alg_prefixfree ==
   722 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   723  (%alg_prefixfree.
   724      list_case True
   725       (%v2. list_case True
   726              (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   727 
   728 lemma alg_prefixfree_primitive_def: "alg_prefixfree =
   729 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   730  (%alg_prefixfree.
   731      list_case True
   732       (%v2. list_case True
   733              (%v6 v7. ~ IS_PREFIX v6 v2 & alg_prefixfree (v6 # v7))))"
   734   by (import prob_canon alg_prefixfree_primitive_def)
   735 
   736 lemma alg_prefixfree_ind: "(All::((bool list list => bool) => bool) => bool)
   737  (%P::bool list list => bool.
   738      (op -->::bool => bool => bool)
   739       ((op &::bool => bool => bool)
   740         ((All::(bool list => bool) => bool)
   741           (%x::bool list.
   742               (All::(bool list => bool) => bool)
   743                (%y::bool list.
   744                    (All::(bool list list => bool) => bool)
   745                     (%z::bool list list.
   746                         (op -->::bool => bool => bool)
   747                          (P ((op #::bool list
   748                                     => bool list list => bool list list)
   749                               y z))
   750                          (P ((op #::bool list
   751                                     => bool list list => bool list list)
   752                               x ((op #::bool list
   753   => bool list list => bool list list)
   754                                   y z)))))))
   755         ((op &::bool => bool => bool)
   756           ((All::(bool list => bool) => bool)
   757             (%v::bool list.
   758                 P ((op #::bool list => bool list list => bool list list) v
   759                     ([]::bool list list))))
   760           (P ([]::bool list list))))
   761       ((All::(bool list list => bool) => bool) P))"
   762   by (import prob_canon alg_prefixfree_ind)
   763 
   764 lemma alg_prefixfree_def: "alg_prefixfree (x # y # z) = (~ IS_PREFIX y x & alg_prefixfree (y # z)) &
   765 alg_prefixfree [v] = True & alg_prefixfree [] = True"
   766   by (import prob_canon alg_prefixfree_def)
   767 
   768 consts
   769   alg_twinfree :: "bool list list => bool" 
   770 
   771 defs
   772   alg_twinfree_primdef: "alg_twinfree ==
   773 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   774  (%alg_twinfree.
   775      list_case True
   776       (%v2. list_case True
   777              (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   778 
   779 lemma alg_twinfree_primitive_def: "alg_twinfree =
   780 WFREC (SOME R. WF R & (ALL x z y. R (y # z) (x # y # z)))
   781  (%alg_twinfree.
   782      list_case True
   783       (%v2. list_case True
   784              (%v6 v7. ~ alg_twin v2 v6 & alg_twinfree (v6 # v7))))"
   785   by (import prob_canon alg_twinfree_primitive_def)
   786 
   787 lemma alg_twinfree_ind: "(All::((bool list list => bool) => bool) => bool)
   788  (%P::bool list list => bool.
   789      (op -->::bool => bool => bool)
   790       ((op &::bool => bool => bool)
   791         ((All::(bool list => bool) => bool)
   792           (%x::bool list.
   793               (All::(bool list => bool) => bool)
   794                (%y::bool list.
   795                    (All::(bool list list => bool) => bool)
   796                     (%z::bool list list.
   797                         (op -->::bool => bool => bool)
   798                          (P ((op #::bool list
   799                                     => bool list list => bool list list)
   800                               y z))
   801                          (P ((op #::bool list
   802                                     => bool list list => bool list list)
   803                               x ((op #::bool list
   804   => bool list list => bool list list)
   805                                   y z)))))))
   806         ((op &::bool => bool => bool)
   807           ((All::(bool list => bool) => bool)
   808             (%v::bool list.
   809                 P ((op #::bool list => bool list list => bool list list) v
   810                     ([]::bool list list))))
   811           (P ([]::bool list list))))
   812       ((All::(bool list list => bool) => bool) P))"
   813   by (import prob_canon alg_twinfree_ind)
   814 
   815 lemma alg_twinfree_def: "alg_twinfree (x # y # z) = (~ alg_twin x y & alg_twinfree (y # z)) &
   816 alg_twinfree [v] = True & alg_twinfree [] = True"
   817   by (import prob_canon alg_twinfree_def)
   818 
   819 consts
   820   alg_longest :: "bool list list => nat" 
   821 
   822 defs
   823   alg_longest_primdef: "alg_longest == FOLDR (%h t. if t <= length h then length h else t) 0"
   824 
   825 lemma alg_longest_def: "alg_longest = FOLDR (%h t. if t <= length h then length h else t) 0"
   826   by (import prob_canon alg_longest_def)
   827 
   828 consts
   829   alg_canon_prefs :: "bool list => bool list list => bool list list" 
   830 
   831 specification (alg_canon_prefs_primdef: alg_canon_prefs) alg_canon_prefs_def: "(ALL l. alg_canon_prefs l [] = [l]) &
   832 (ALL l h t.
   833     alg_canon_prefs l (h # t) =
   834     (if IS_PREFIX h l then alg_canon_prefs l t else l # h # t))"
   835   by (import prob_canon alg_canon_prefs_def)
   836 
   837 consts
   838   alg_canon_find :: "bool list => bool list list => bool list list" 
   839 
   840 specification (alg_canon_find_primdef: alg_canon_find) alg_canon_find_def: "(ALL l. alg_canon_find l [] = [l]) &
   841 (ALL l h t.
   842     alg_canon_find l (h # t) =
   843     (if alg_order h l
   844      then if IS_PREFIX l h then h # t else h # alg_canon_find l t
   845      else alg_canon_prefs l (h # t)))"
   846   by (import prob_canon alg_canon_find_def)
   847 
   848 consts
   849   alg_canon1 :: "bool list list => bool list list" 
   850 
   851 defs
   852   alg_canon1_primdef: "alg_canon1 == FOLDR alg_canon_find []"
   853 
   854 lemma alg_canon1_def: "alg_canon1 = FOLDR alg_canon_find []"
   855   by (import prob_canon alg_canon1_def)
   856 
   857 consts
   858   alg_canon_merge :: "bool list => bool list list => bool list list" 
   859 
   860 specification (alg_canon_merge_primdef: alg_canon_merge) alg_canon_merge_def: "(ALL l. alg_canon_merge l [] = [l]) &
   861 (ALL l h t.
   862     alg_canon_merge l (h # t) =
   863     (if alg_twin l h then alg_canon_merge (butlast h) t else l # h # t))"
   864   by (import prob_canon alg_canon_merge_def)
   865 
   866 consts
   867   alg_canon2 :: "bool list list => bool list list" 
   868 
   869 defs
   870   alg_canon2_primdef: "alg_canon2 == FOLDR alg_canon_merge []"
   871 
   872 lemma alg_canon2_def: "alg_canon2 = FOLDR alg_canon_merge []"
   873   by (import prob_canon alg_canon2_def)
   874 
   875 consts
   876   alg_canon :: "bool list list => bool list list" 
   877 
   878 defs
   879   alg_canon_primdef: "alg_canon == %l. alg_canon2 (alg_canon1 l)"
   880 
   881 lemma alg_canon_def: "ALL l. alg_canon l = alg_canon2 (alg_canon1 l)"
   882   by (import prob_canon alg_canon_def)
   883 
   884 consts
   885   algebra_canon :: "bool list list => bool" 
   886 
   887 defs
   888   algebra_canon_primdef: "algebra_canon == %l. alg_canon l = l"
   889 
   890 lemma algebra_canon_def: "ALL l. algebra_canon l = (alg_canon l = l)"
   891   by (import prob_canon algebra_canon_def)
   892 
   893 lemma ALG_TWIN_NIL: "ALL l. ~ alg_twin l [] & ~ alg_twin [] l"
   894   by (import prob_canon ALG_TWIN_NIL)
   895 
   896 lemma ALG_TWIN_SING: "ALL x l.
   897    alg_twin [x] l = (x = True & l = [False]) &
   898    alg_twin l [x] = (l = [True] & x = False)"
   899   by (import prob_canon ALG_TWIN_SING)
   900 
   901 lemma ALG_TWIN_CONS: "ALL x y z h t.
   902    alg_twin (x # y # z) (h # t) = (x = h & alg_twin (y # z) t) &
   903    alg_twin (h # t) (x # y # z) = (x = h & alg_twin t (y # z))"
   904   by (import prob_canon ALG_TWIN_CONS)
   905 
   906 lemma ALG_TWIN_REDUCE: "ALL h t t'. alg_twin (h # t) (h # t') = alg_twin t t'"
   907   by (import prob_canon ALG_TWIN_REDUCE)
   908 
   909 lemma ALG_TWINS_PREFIX: "(All::(bool list => bool) => bool)
   910  (%x::bool list.
   911      (All::(bool list => bool) => bool)
   912       (%l::bool list.
   913           (op -->::bool => bool => bool)
   914            ((IS_PREFIX::bool list => bool list => bool) x l)
   915            ((op |::bool => bool => bool)
   916              ((op =::bool list => bool list => bool) x l)
   917              ((op |::bool => bool => bool)
   918                ((IS_PREFIX::bool list => bool list => bool) x
   919                  ((SNOC::bool => bool list => bool list) (True::bool) l))
   920                ((IS_PREFIX::bool list => bool list => bool) x
   921                  ((SNOC::bool => bool list => bool list) (False::bool)
   922                    l))))))"
   923   by (import prob_canon ALG_TWINS_PREFIX)
   924 
   925 lemma ALG_ORDER_NIL: "ALL x. alg_order [] x & alg_order x [] = (x = [])"
   926   by (import prob_canon ALG_ORDER_NIL)
   927 
   928 lemma ALG_ORDER_REFL: "ALL x. alg_order x x"
   929   by (import prob_canon ALG_ORDER_REFL)
   930 
   931 lemma ALG_ORDER_ANTISYM: "(All::(bool list => bool) => bool)
   932  (%x::bool list.
   933      (All::(bool list => bool) => bool)
   934       (%y::bool list.
   935           (op -->::bool => bool => bool)
   936            ((op &::bool => bool => bool)
   937              ((alg_order::bool list => bool list => bool) x y)
   938              ((alg_order::bool list => bool list => bool) y x))
   939            ((op =::bool list => bool list => bool) x y)))"
   940   by (import prob_canon ALG_ORDER_ANTISYM)
   941 
   942 lemma ALG_ORDER_TRANS: "(All::(bool list => bool) => bool)
   943  (%x::bool list.
   944      (All::(bool list => bool) => bool)
   945       (%y::bool list.
   946           (All::(bool list => bool) => bool)
   947            (%z::bool list.
   948                (op -->::bool => bool => bool)
   949                 ((op &::bool => bool => bool)
   950                   ((alg_order::bool list => bool list => bool) x y)
   951                   ((alg_order::bool list => bool list => bool) y z))
   952                 ((alg_order::bool list => bool list => bool) x z))))"
   953   by (import prob_canon ALG_ORDER_TRANS)
   954 
   955 lemma ALG_ORDER_TOTAL: "ALL x y. alg_order x y | alg_order y x"
   956   by (import prob_canon ALG_ORDER_TOTAL)
   957 
   958 lemma ALG_ORDER_PREFIX: "(All::(bool list => bool) => bool)
   959  (%x::bool list.
   960      (All::(bool list => bool) => bool)
   961       (%y::bool list.
   962           (op -->::bool => bool => bool)
   963            ((IS_PREFIX::bool list => bool list => bool) y x)
   964            ((alg_order::bool list => bool list => bool) x y)))"
   965   by (import prob_canon ALG_ORDER_PREFIX)
   966 
   967 lemma ALG_ORDER_PREFIX_ANTI: "(All::(bool list => bool) => bool)
   968  (%x::bool list.
   969      (All::(bool list => bool) => bool)
   970       (%y::bool list.
   971           (op -->::bool => bool => bool)
   972            ((op &::bool => bool => bool)
   973              ((alg_order::bool list => bool list => bool) x y)
   974              ((IS_PREFIX::bool list => bool list => bool) x y))
   975            ((op =::bool list => bool list => bool) x y)))"
   976   by (import prob_canon ALG_ORDER_PREFIX_ANTI)
   977 
   978 lemma ALG_ORDER_PREFIX_MONO: "(All::(bool list => bool) => bool)
   979  (%x::bool list.
   980      (All::(bool list => bool) => bool)
   981       (%y::bool list.
   982           (All::(bool list => bool) => bool)
   983            (%z::bool list.
   984                (op -->::bool => bool => bool)
   985                 ((op &::bool => bool => bool)
   986                   ((alg_order::bool list => bool list => bool) x y)
   987                   ((op &::bool => bool => bool)
   988                     ((alg_order::bool list => bool list => bool) y z)
   989                     ((IS_PREFIX::bool list => bool list => bool) z x)))
   990                 ((IS_PREFIX::bool list => bool list => bool) y x))))"
   991   by (import prob_canon ALG_ORDER_PREFIX_MONO)
   992 
   993 lemma ALG_ORDER_PREFIX_TRANS: "(All::(bool list => bool) => bool)
   994  (%x::bool list.
   995      (All::(bool list => bool) => bool)
   996       (%y::bool list.
   997           (All::(bool list => bool) => bool)
   998            (%z::bool list.
   999                (op -->::bool => bool => bool)
  1000                 ((op &::bool => bool => bool)
  1001                   ((alg_order::bool list => bool list => bool) x y)
  1002                   ((IS_PREFIX::bool list => bool list => bool) y z))
  1003                 ((op |::bool => bool => bool)
  1004                   ((alg_order::bool list => bool list => bool) x z)
  1005                   ((IS_PREFIX::bool list => bool list => bool) x z)))))"
  1006   by (import prob_canon ALG_ORDER_PREFIX_TRANS)
  1007 
  1008 lemma ALG_ORDER_SNOC: "ALL x l. ~ alg_order (SNOC x l) l"
  1009   by (import prob_canon ALG_ORDER_SNOC)
  1010 
  1011 lemma ALG_SORTED_MIN: "(All::(bool list => bool) => bool)
  1012  (%h::bool list.
  1013      (All::(bool list list => bool) => bool)
  1014       (%t::bool list list.
  1015           (op -->::bool => bool => bool)
  1016            ((alg_sorted::bool list list => bool)
  1017              ((op #::bool list => bool list list => bool list list) h t))
  1018            ((All::(bool list => bool) => bool)
  1019              (%x::bool list.
  1020                  (op -->::bool => bool => bool)
  1021                   ((op mem::bool list => bool list list => bool) x t)
  1022                   ((alg_order::bool list => bool list => bool) h x)))))"
  1023   by (import prob_canon ALG_SORTED_MIN)
  1024 
  1025 lemma ALG_SORTED_DEF_ALT: "(All::(bool list => bool) => bool)
  1026  (%h::bool list.
  1027      (All::(bool list list => bool) => bool)
  1028       (%t::bool list list.
  1029           (op =::bool => bool => bool)
  1030            ((alg_sorted::bool list list => bool)
  1031              ((op #::bool list => bool list list => bool list list) h t))
  1032            ((op &::bool => bool => bool)
  1033              ((All::(bool list => bool) => bool)
  1034                (%x::bool list.
  1035                    (op -->::bool => bool => bool)
  1036                     ((op mem::bool list => bool list list => bool) x t)
  1037                     ((alg_order::bool list => bool list => bool) h x)))
  1038              ((alg_sorted::bool list list => bool) t))))"
  1039   by (import prob_canon ALG_SORTED_DEF_ALT)
  1040 
  1041 lemma ALG_SORTED_TL: "(All::(bool list => bool) => bool)
  1042  (%h::bool list.
  1043      (All::(bool list list => bool) => bool)
  1044       (%t::bool list list.
  1045           (op -->::bool => bool => bool)
  1046            ((alg_sorted::bool list list => bool)
  1047              ((op #::bool list => bool list list => bool list list) h t))
  1048            ((alg_sorted::bool list list => bool) t)))"
  1049   by (import prob_canon ALG_SORTED_TL)
  1050 
  1051 lemma ALG_SORTED_MONO: "(All::(bool list => bool) => bool)
  1052  (%x::bool list.
  1053      (All::(bool list => bool) => bool)
  1054       (%y::bool list.
  1055           (All::(bool list list => bool) => bool)
  1056            (%z::bool list list.
  1057                (op -->::bool => bool => bool)
  1058                 ((alg_sorted::bool list list => bool)
  1059                   ((op #::bool list => bool list list => bool list list) x
  1060                     ((op #::bool list => bool list list => bool list list) y
  1061                       z)))
  1062                 ((alg_sorted::bool list list => bool)
  1063                   ((op #::bool list => bool list list => bool list list) x
  1064                     z)))))"
  1065   by (import prob_canon ALG_SORTED_MONO)
  1066 
  1067 lemma ALG_SORTED_TLS: "ALL l b. alg_sorted (map (op # b) l) = alg_sorted l"
  1068   by (import prob_canon ALG_SORTED_TLS)
  1069 
  1070 lemma ALG_SORTED_STEP: "ALL l1 l2.
  1071    alg_sorted (map (op # True) l1 @ map (op # False) l2) =
  1072    (alg_sorted l1 & alg_sorted l2)"
  1073   by (import prob_canon ALG_SORTED_STEP)
  1074 
  1075 lemma ALG_SORTED_APPEND: "ALL h h' t t'.
  1076    alg_sorted ((h # t) @ h' # t') =
  1077    (alg_sorted (h # t) & alg_sorted (h' # t') & alg_order (last (h # t)) h')"
  1078   by (import prob_canon ALG_SORTED_APPEND)
  1079 
  1080 lemma ALG_SORTED_FILTER: "(All::((bool list => bool) => bool) => bool)
  1081  (%P::bool list => bool.
  1082      (All::(bool list list => bool) => bool)
  1083       (%b::bool list list.
  1084           (op -->::bool => bool => bool)
  1085            ((alg_sorted::bool list list => bool) b)
  1086            ((alg_sorted::bool list list => bool)
  1087              ((filter::(bool list => bool)
  1088                        => bool list list => bool list list)
  1089                P b))))"
  1090   by (import prob_canon ALG_SORTED_FILTER)
  1091 
  1092 lemma ALG_PREFIXFREE_TL: "(All::(bool list => bool) => bool)
  1093  (%h::bool list.
  1094      (All::(bool list list => bool) => bool)
  1095       (%t::bool list list.
  1096           (op -->::bool => bool => bool)
  1097            ((alg_prefixfree::bool list list => bool)
  1098              ((op #::bool list => bool list list => bool list list) h t))
  1099            ((alg_prefixfree::bool list list => bool) t)))"
  1100   by (import prob_canon ALG_PREFIXFREE_TL)
  1101 
  1102 lemma ALG_PREFIXFREE_MONO: "(All::(bool list => bool) => bool)
  1103  (%x::bool list.
  1104      (All::(bool list => bool) => bool)
  1105       (%y::bool list.
  1106           (All::(bool list list => bool) => bool)
  1107            (%z::bool list list.
  1108                (op -->::bool => bool => bool)
  1109                 ((op &::bool => bool => bool)
  1110                   ((alg_sorted::bool list list => bool)
  1111                     ((op #::bool list => bool list list => bool list list) x
  1112                       ((op #::bool list => bool list list => bool list list)
  1113                         y z)))
  1114                   ((alg_prefixfree::bool list list => bool)
  1115                     ((op #::bool list => bool list list => bool list list) x
  1116                       ((op #::bool list => bool list list => bool list list)
  1117                         y z))))
  1118                 ((alg_prefixfree::bool list list => bool)
  1119                   ((op #::bool list => bool list list => bool list list) x
  1120                     z)))))"
  1121   by (import prob_canon ALG_PREFIXFREE_MONO)
  1122 
  1123 lemma ALG_PREFIXFREE_ELT: "(All::(bool list => bool) => bool)
  1124  (%h::bool list.
  1125      (All::(bool list list => bool) => bool)
  1126       (%t::bool list list.
  1127           (op -->::bool => bool => bool)
  1128            ((op &::bool => bool => bool)
  1129              ((alg_sorted::bool list list => bool)
  1130                ((op #::bool list => bool list list => bool list list) h t))
  1131              ((alg_prefixfree::bool list list => bool)
  1132                ((op #::bool list => bool list list => bool list list) h t)))
  1133            ((All::(bool list => bool) => bool)
  1134              (%x::bool list.
  1135                  (op -->::bool => bool => bool)
  1136                   ((op mem::bool list => bool list list => bool) x t)
  1137                   ((op &::bool => bool => bool)
  1138                     ((Not::bool => bool)
  1139                       ((IS_PREFIX::bool list => bool list => bool) x h))
  1140                     ((Not::bool => bool)
  1141                       ((IS_PREFIX::bool list => bool list => bool) h
  1142                         x)))))))"
  1143   by (import prob_canon ALG_PREFIXFREE_ELT)
  1144 
  1145 lemma ALG_PREFIXFREE_TLS: "ALL l b. alg_prefixfree (map (op # b) l) = alg_prefixfree l"
  1146   by (import prob_canon ALG_PREFIXFREE_TLS)
  1147 
  1148 lemma ALG_PREFIXFREE_STEP: "ALL l1 l2.
  1149    alg_prefixfree (map (op # True) l1 @ map (op # False) l2) =
  1150    (alg_prefixfree l1 & alg_prefixfree l2)"
  1151   by (import prob_canon ALG_PREFIXFREE_STEP)
  1152 
  1153 lemma ALG_PREFIXFREE_APPEND: "ALL h h' t t'.
  1154    alg_prefixfree ((h # t) @ h' # t') =
  1155    (alg_prefixfree (h # t) &
  1156     alg_prefixfree (h' # t') & ~ IS_PREFIX h' (last (h # t)))"
  1157   by (import prob_canon ALG_PREFIXFREE_APPEND)
  1158 
  1159 lemma ALG_PREFIXFREE_FILTER: "(All::((bool list => bool) => bool) => bool)
  1160  (%P::bool list => bool.
  1161      (All::(bool list list => bool) => bool)
  1162       (%b::bool list list.
  1163           (op -->::bool => bool => bool)
  1164            ((op &::bool => bool => bool)
  1165              ((alg_sorted::bool list list => bool) b)
  1166              ((alg_prefixfree::bool list list => bool) b))
  1167            ((alg_prefixfree::bool list list => bool)
  1168              ((filter::(bool list => bool)
  1169                        => bool list list => bool list list)
  1170                P b))))"
  1171   by (import prob_canon ALG_PREFIXFREE_FILTER)
  1172 
  1173 lemma ALG_TWINFREE_TL: "(All::(bool list => bool) => bool)
  1174  (%h::bool list.
  1175      (All::(bool list list => bool) => bool)
  1176       (%t::bool list list.
  1177           (op -->::bool => bool => bool)
  1178            ((alg_twinfree::bool list list => bool)
  1179              ((op #::bool list => bool list list => bool list list) h t))
  1180            ((alg_twinfree::bool list list => bool) t)))"
  1181   by (import prob_canon ALG_TWINFREE_TL)
  1182 
  1183 lemma ALG_TWINFREE_TLS: "ALL l b. alg_twinfree (map (op # b) l) = alg_twinfree l"
  1184   by (import prob_canon ALG_TWINFREE_TLS)
  1185 
  1186 lemma ALG_TWINFREE_STEP1: "(All::(bool list list => bool) => bool)
  1187  (%l1::bool list list.
  1188      (All::(bool list list => bool) => bool)
  1189       (%l2::bool list list.
  1190           (op -->::bool => bool => bool)
  1191            ((alg_twinfree::bool list list => bool)
  1192              ((op @::bool list list => bool list list => bool list list)
  1193                ((map::(bool list => bool list)
  1194                       => bool list list => bool list list)
  1195                  ((op #::bool => bool list => bool list) (True::bool)) l1)
  1196                ((map::(bool list => bool list)
  1197                       => bool list list => bool list list)
  1198                  ((op #::bool => bool list => bool list) (False::bool))
  1199                  l2)))
  1200            ((op &::bool => bool => bool)
  1201              ((alg_twinfree::bool list list => bool) l1)
  1202              ((alg_twinfree::bool list list => bool) l2))))"
  1203   by (import prob_canon ALG_TWINFREE_STEP1)
  1204 
  1205 lemma ALG_TWINFREE_STEP2: "(All::(bool list list => bool) => bool)
  1206  (%l1::bool list list.
  1207      (All::(bool list list => bool) => bool)
  1208       (%l2::bool list list.
  1209           (op -->::bool => bool => bool)
  1210            ((op &::bool => bool => bool)
  1211              ((op |::bool => bool => bool)
  1212                ((Not::bool => bool)
  1213                  ((op mem::bool list => bool list list => bool)
  1214                    ([]::bool list) l1))
  1215                ((Not::bool => bool)
  1216                  ((op mem::bool list => bool list list => bool)
  1217                    ([]::bool list) l2)))
  1218              ((op &::bool => bool => bool)
  1219                ((alg_twinfree::bool list list => bool) l1)
  1220                ((alg_twinfree::bool list list => bool) l2)))
  1221            ((alg_twinfree::bool list list => bool)
  1222              ((op @::bool list list => bool list list => bool list list)
  1223                ((map::(bool list => bool list)
  1224                       => bool list list => bool list list)
  1225                  ((op #::bool => bool list => bool list) (True::bool)) l1)
  1226                ((map::(bool list => bool list)
  1227                       => bool list list => bool list list)
  1228                  ((op #::bool => bool list => bool list) (False::bool))
  1229                  l2)))))"
  1230   by (import prob_canon ALG_TWINFREE_STEP2)
  1231 
  1232 lemma ALG_TWINFREE_STEP: "(All::(bool list list => bool) => bool)
  1233  (%l1::bool list list.
  1234      (All::(bool list list => bool) => bool)
  1235       (%l2::bool list list.
  1236           (op -->::bool => bool => bool)
  1237            ((op |::bool => bool => bool)
  1238              ((Not::bool => bool)
  1239                ((op mem::bool list => bool list list => bool)
  1240                  ([]::bool list) l1))
  1241              ((Not::bool => bool)
  1242                ((op mem::bool list => bool list list => bool)
  1243                  ([]::bool list) l2)))
  1244            ((op =::bool => bool => bool)
  1245              ((alg_twinfree::bool list list => bool)
  1246                ((op @::bool list list => bool list list => bool list list)
  1247                  ((map::(bool list => bool list)
  1248                         => bool list list => bool list list)
  1249                    ((op #::bool => bool list => bool list) (True::bool)) l1)
  1250                  ((map::(bool list => bool list)
  1251                         => bool list list => bool list list)
  1252                    ((op #::bool => bool list => bool list) (False::bool))
  1253                    l2)))
  1254              ((op &::bool => bool => bool)
  1255                ((alg_twinfree::bool list list => bool) l1)
  1256                ((alg_twinfree::bool list list => bool) l2)))))"
  1257   by (import prob_canon ALG_TWINFREE_STEP)
  1258 
  1259 lemma ALG_LONGEST_HD: "ALL h t. length h <= alg_longest (h # t)"
  1260   by (import prob_canon ALG_LONGEST_HD)
  1261 
  1262 lemma ALG_LONGEST_TL: "ALL h t. alg_longest t <= alg_longest (h # t)"
  1263   by (import prob_canon ALG_LONGEST_TL)
  1264 
  1265 lemma ALG_LONGEST_TLS: "ALL h t b. alg_longest (map (op # b) (h # t)) = Suc (alg_longest (h # t))"
  1266   by (import prob_canon ALG_LONGEST_TLS)
  1267 
  1268 lemma ALG_LONGEST_APPEND: "ALL l1 l2.
  1269    alg_longest l1 <= alg_longest (l1 @ l2) &
  1270    alg_longest l2 <= alg_longest (l1 @ l2)"
  1271   by (import prob_canon ALG_LONGEST_APPEND)
  1272 
  1273 lemma ALG_CANON_PREFS_HD: "ALL l b. hd (alg_canon_prefs l b) = l"
  1274   by (import prob_canon ALG_CANON_PREFS_HD)
  1275 
  1276 lemma ALG_CANON_PREFS_DELETES: "(All::(bool list => bool) => bool)
  1277  (%l::bool list.
  1278      (All::(bool list list => bool) => bool)
  1279       (%b::bool list list.
  1280           (All::(bool list => bool) => bool)
  1281            (%x::bool list.
  1282                (op -->::bool => bool => bool)
  1283                 ((op mem::bool list => bool list list => bool) x
  1284                   ((alg_canon_prefs::bool list
  1285                                      => bool list list => bool list list)
  1286                     l b))
  1287                 ((op mem::bool list => bool list list => bool) x
  1288                   ((op #::bool list => bool list list => bool list list) l
  1289                     b)))))"
  1290   by (import prob_canon ALG_CANON_PREFS_DELETES)
  1291 
  1292 lemma ALG_CANON_PREFS_SORTED: "(All::(bool list => bool) => bool)
  1293  (%l::bool list.
  1294      (All::(bool list list => bool) => bool)
  1295       (%b::bool list list.
  1296           (op -->::bool => bool => bool)
  1297            ((alg_sorted::bool list list => bool)
  1298              ((op #::bool list => bool list list => bool list list) l b))
  1299            ((alg_sorted::bool list list => bool)
  1300              ((alg_canon_prefs::bool list
  1301                                 => bool list list => bool list list)
  1302                l b))))"
  1303   by (import prob_canon ALG_CANON_PREFS_SORTED)
  1304 
  1305 lemma ALG_CANON_PREFS_PREFIXFREE: "(All::(bool list => bool) => bool)
  1306  (%l::bool list.
  1307      (All::(bool list list => bool) => bool)
  1308       (%b::bool list list.
  1309           (op -->::bool => bool => bool)
  1310            ((op &::bool => bool => bool)
  1311              ((alg_sorted::bool list list => bool) b)
  1312              ((alg_prefixfree::bool list list => bool) b))
  1313            ((alg_prefixfree::bool list list => bool)
  1314              ((alg_canon_prefs::bool list
  1315                                 => bool list list => bool list list)
  1316                l b))))"
  1317   by (import prob_canon ALG_CANON_PREFS_PREFIXFREE)
  1318 
  1319 lemma ALG_CANON_PREFS_CONSTANT: "(All::(bool list => bool) => bool)
  1320  (%l::bool list.
  1321      (All::(bool list list => bool) => bool)
  1322       (%b::bool list list.
  1323           (op -->::bool => bool => bool)
  1324            ((alg_prefixfree::bool list list => bool)
  1325              ((op #::bool list => bool list list => bool list list) l b))
  1326            ((op =::bool list list => bool list list => bool)
  1327              ((alg_canon_prefs::bool list
  1328                                 => bool list list => bool list list)
  1329                l b)
  1330              ((op #::bool list => bool list list => bool list list) l b))))"
  1331   by (import prob_canon ALG_CANON_PREFS_CONSTANT)
  1332 
  1333 lemma ALG_CANON_FIND_HD: "ALL l h t.
  1334    hd (alg_canon_find l (h # t)) = l | hd (alg_canon_find l (h # t)) = h"
  1335   by (import prob_canon ALG_CANON_FIND_HD)
  1336 
  1337 lemma ALG_CANON_FIND_DELETES: "(All::(bool list => bool) => bool)
  1338  (%l::bool list.
  1339      (All::(bool list list => bool) => bool)
  1340       (%b::bool list list.
  1341           (All::(bool list => bool) => bool)
  1342            (%x::bool list.
  1343                (op -->::bool => bool => bool)
  1344                 ((op mem::bool list => bool list list => bool) x
  1345                   ((alg_canon_find::bool list
  1346                                     => bool list list => bool list list)
  1347                     l b))
  1348                 ((op mem::bool list => bool list list => bool) x
  1349                   ((op #::bool list => bool list list => bool list list) l
  1350                     b)))))"
  1351   by (import prob_canon ALG_CANON_FIND_DELETES)
  1352 
  1353 lemma ALG_CANON_FIND_SORTED: "(All::(bool list => bool) => bool)
  1354  (%l::bool list.
  1355      (All::(bool list list => bool) => bool)
  1356       (%b::bool list list.
  1357           (op -->::bool => bool => bool)
  1358            ((alg_sorted::bool list list => bool) b)
  1359            ((alg_sorted::bool list list => bool)
  1360              ((alg_canon_find::bool list
  1361                                => bool list list => bool list list)
  1362                l b))))"
  1363   by (import prob_canon ALG_CANON_FIND_SORTED)
  1364 
  1365 lemma ALG_CANON_FIND_PREFIXFREE: "(All::(bool list => bool) => bool)
  1366  (%l::bool list.
  1367      (All::(bool list list => bool) => bool)
  1368       (%b::bool list list.
  1369           (op -->::bool => bool => bool)
  1370            ((op &::bool => bool => bool)
  1371              ((alg_sorted::bool list list => bool) b)
  1372              ((alg_prefixfree::bool list list => bool) b))
  1373            ((alg_prefixfree::bool list list => bool)
  1374              ((alg_canon_find::bool list
  1375                                => bool list list => bool list list)
  1376                l b))))"
  1377   by (import prob_canon ALG_CANON_FIND_PREFIXFREE)
  1378 
  1379 lemma ALG_CANON_FIND_CONSTANT: "(All::(bool list => bool) => bool)
  1380  (%l::bool list.
  1381      (All::(bool list list => bool) => bool)
  1382       (%b::bool list list.
  1383           (op -->::bool => bool => bool)
  1384            ((op &::bool => bool => bool)
  1385              ((alg_sorted::bool list list => bool)
  1386                ((op #::bool list => bool list list => bool list list) l b))
  1387              ((alg_prefixfree::bool list list => bool)
  1388                ((op #::bool list => bool list list => bool list list) l b)))
  1389            ((op =::bool list list => bool list list => bool)
  1390              ((alg_canon_find::bool list
  1391                                => bool list list => bool list list)
  1392                l b)
  1393              ((op #::bool list => bool list list => bool list list) l b))))"
  1394   by (import prob_canon ALG_CANON_FIND_CONSTANT)
  1395 
  1396 lemma ALG_CANON1_SORTED: "ALL x. alg_sorted (alg_canon1 x)"
  1397   by (import prob_canon ALG_CANON1_SORTED)
  1398 
  1399 lemma ALG_CANON1_PREFIXFREE: "ALL l. alg_prefixfree (alg_canon1 l)"
  1400   by (import prob_canon ALG_CANON1_PREFIXFREE)
  1401 
  1402 lemma ALG_CANON1_CONSTANT: "(All::(bool list list => bool) => bool)
  1403  (%l::bool list list.
  1404      (op -->::bool => bool => bool)
  1405       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
  1406         ((alg_prefixfree::bool list list => bool) l))
  1407       ((op =::bool list list => bool list list => bool)
  1408         ((alg_canon1::bool list list => bool list list) l) l))"
  1409   by (import prob_canon ALG_CANON1_CONSTANT)
  1410 
  1411 lemma ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list => bool) => bool)
  1412  (%l::bool list.
  1413      (All::(bool list list => bool) => bool)
  1414       (%b::bool list list.
  1415           (op -->::bool => bool => bool)
  1416            ((op &::bool => bool => bool)
  1417              ((alg_sorted::bool list list => bool)
  1418                ((op #::bool list => bool list list => bool list list) l b))
  1419              ((op &::bool => bool => bool)
  1420                ((alg_prefixfree::bool list list => bool)
  1421                  ((op #::bool list => bool list list => bool list list) l
  1422                    b))
  1423                ((alg_twinfree::bool list list => bool) b)))
  1424            ((op &::bool => bool => bool)
  1425              ((alg_sorted::bool list list => bool)
  1426                ((alg_canon_merge::bool list
  1427                                   => bool list list => bool list list)
  1428                  l b))
  1429              ((op &::bool => bool => bool)
  1430                ((alg_prefixfree::bool list list => bool)
  1431                  ((alg_canon_merge::bool list
  1432                                     => bool list list => bool list list)
  1433                    l b))
  1434                ((alg_twinfree::bool list list => bool)
  1435                  ((alg_canon_merge::bool list
  1436                                     => bool list list => bool list list)
  1437                    l b))))))"
  1438   by (import prob_canon ALG_CANON_MERGE_SORTED_PREFIXFREE_TWINFREE)
  1439 
  1440 lemma ALG_CANON_MERGE_PREFIXFREE_PRESERVE: "(All::(bool list => bool) => bool)
  1441  (%l::bool list.
  1442      (All::(bool list list => bool) => bool)
  1443       (%b::bool list list.
  1444           (All::(bool list => bool) => bool)
  1445            (%h::bool list.
  1446                (op -->::bool => bool => bool)
  1447                 ((All::(bool list => bool) => bool)
  1448                   (%x::bool list.
  1449                       (op -->::bool => bool => bool)
  1450                        ((op mem::bool list => bool list list => bool) x
  1451                          ((op #::bool list
  1452                                  => bool list list => bool list list)
  1453                            l b))
  1454                        ((op &::bool => bool => bool)
  1455                          ((Not::bool => bool)
  1456                            ((IS_PREFIX::bool list => bool list => bool) h
  1457                              x))
  1458                          ((Not::bool => bool)
  1459                            ((IS_PREFIX::bool list => bool list => bool) x
  1460                              h)))))
  1461                 ((All::(bool list => bool) => bool)
  1462                   (%x::bool list.
  1463                       (op -->::bool => bool => bool)
  1464                        ((op mem::bool list => bool list list => bool) x
  1465                          ((alg_canon_merge::bool list
  1466       => bool list list => bool list list)
  1467                            l b))
  1468                        ((op &::bool => bool => bool)
  1469                          ((Not::bool => bool)
  1470                            ((IS_PREFIX::bool list => bool list => bool) h
  1471                              x))
  1472                          ((Not::bool => bool)
  1473                            ((IS_PREFIX::bool list => bool list => bool) x
  1474                              h))))))))"
  1475   by (import prob_canon ALG_CANON_MERGE_PREFIXFREE_PRESERVE)
  1476 
  1477 lemma ALG_CANON_MERGE_SHORTENS: "(All::(bool list => bool) => bool)
  1478  (%l::bool list.
  1479      (All::(bool list list => bool) => bool)
  1480       (%b::bool list list.
  1481           (All::(bool list => bool) => bool)
  1482            (%x::bool list.
  1483                (op -->::bool => bool => bool)
  1484                 ((op mem::bool list => bool list list => bool) x
  1485                   ((alg_canon_merge::bool list
  1486                                      => bool list list => bool list list)
  1487                     l b))
  1488                 ((Ex::(bool list => bool) => bool)
  1489                   (%y::bool list.
  1490                       (op &::bool => bool => bool)
  1491                        ((op mem::bool list => bool list list => bool) y
  1492                          ((op #::bool list
  1493                                  => bool list list => bool list list)
  1494                            l b))
  1495                        ((IS_PREFIX::bool list => bool list => bool) y
  1496                          x))))))"
  1497   by (import prob_canon ALG_CANON_MERGE_SHORTENS)
  1498 
  1499 lemma ALG_CANON_MERGE_CONSTANT: "(All::(bool list => bool) => bool)
  1500  (%l::bool list.
  1501      (All::(bool list list => bool) => bool)
  1502       (%b::bool list list.
  1503           (op -->::bool => bool => bool)
  1504            ((alg_twinfree::bool list list => bool)
  1505              ((op #::bool list => bool list list => bool list list) l b))
  1506            ((op =::bool list list => bool list list => bool)
  1507              ((alg_canon_merge::bool list
  1508                                 => bool list list => bool list list)
  1509                l b)
  1510              ((op #::bool list => bool list list => bool list list) l b))))"
  1511   by (import prob_canon ALG_CANON_MERGE_CONSTANT)
  1512 
  1513 lemma ALG_CANON2_PREFIXFREE_PRESERVE: "(All::(bool list list => bool) => bool)
  1514  (%x::bool list list.
  1515      (All::(bool list => bool) => bool)
  1516       (%xa::bool list.
  1517           (op -->::bool => bool => bool)
  1518            ((All::(bool list => bool) => bool)
  1519              (%xb::bool list.
  1520                  (op -->::bool => bool => bool)
  1521                   ((op mem::bool list => bool list list => bool) xb x)
  1522                   ((op &::bool => bool => bool)
  1523                     ((Not::bool => bool)
  1524                       ((IS_PREFIX::bool list => bool list => bool) xa xb))
  1525                     ((Not::bool => bool)
  1526                       ((IS_PREFIX::bool list => bool list => bool) xb
  1527                         xa)))))
  1528            ((All::(bool list => bool) => bool)
  1529              (%xb::bool list.
  1530                  (op -->::bool => bool => bool)
  1531                   ((op mem::bool list => bool list list => bool) xb
  1532                     ((alg_canon2::bool list list => bool list list) x))
  1533                   ((op &::bool => bool => bool)
  1534                     ((Not::bool => bool)
  1535                       ((IS_PREFIX::bool list => bool list => bool) xa xb))
  1536                     ((Not::bool => bool)
  1537                       ((IS_PREFIX::bool list => bool list => bool) xb
  1538                         xa)))))))"
  1539   by (import prob_canon ALG_CANON2_PREFIXFREE_PRESERVE)
  1540 
  1541 lemma ALG_CANON2_SHORTENS: "(All::(bool list list => bool) => bool)
  1542  (%x::bool list list.
  1543      (All::(bool list => bool) => bool)
  1544       (%xa::bool list.
  1545           (op -->::bool => bool => bool)
  1546            ((op mem::bool list => bool list list => bool) xa
  1547              ((alg_canon2::bool list list => bool list list) x))
  1548            ((Ex::(bool list => bool) => bool)
  1549              (%y::bool list.
  1550                  (op &::bool => bool => bool)
  1551                   ((op mem::bool list => bool list list => bool) y x)
  1552                   ((IS_PREFIX::bool list => bool list => bool) y xa)))))"
  1553   by (import prob_canon ALG_CANON2_SHORTENS)
  1554 
  1555 lemma ALG_CANON2_SORTED_PREFIXFREE_TWINFREE: "(All::(bool list list => bool) => bool)
  1556  (%x::bool list list.
  1557      (op -->::bool => bool => bool)
  1558       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) x)
  1559         ((alg_prefixfree::bool list list => bool) x))
  1560       ((op &::bool => bool => bool)
  1561         ((alg_sorted::bool list list => bool)
  1562           ((alg_canon2::bool list list => bool list list) x))
  1563         ((op &::bool => bool => bool)
  1564           ((alg_prefixfree::bool list list => bool)
  1565             ((alg_canon2::bool list list => bool list list) x))
  1566           ((alg_twinfree::bool list list => bool)
  1567             ((alg_canon2::bool list list => bool list list) x)))))"
  1568   by (import prob_canon ALG_CANON2_SORTED_PREFIXFREE_TWINFREE)
  1569 
  1570 lemma ALG_CANON2_CONSTANT: "(All::(bool list list => bool) => bool)
  1571  (%l::bool list list.
  1572      (op -->::bool => bool => bool)
  1573       ((alg_twinfree::bool list list => bool) l)
  1574       ((op =::bool list list => bool list list => bool)
  1575         ((alg_canon2::bool list list => bool list list) l) l))"
  1576   by (import prob_canon ALG_CANON2_CONSTANT)
  1577 
  1578 lemma ALG_CANON_SORTED_PREFIXFREE_TWINFREE: "ALL l.
  1579    alg_sorted (alg_canon l) &
  1580    alg_prefixfree (alg_canon l) & alg_twinfree (alg_canon l)"
  1581   by (import prob_canon ALG_CANON_SORTED_PREFIXFREE_TWINFREE)
  1582 
  1583 lemma ALG_CANON_CONSTANT: "(All::(bool list list => bool) => bool)
  1584  (%l::bool list list.
  1585      (op -->::bool => bool => bool)
  1586       ((op &::bool => bool => bool) ((alg_sorted::bool list list => bool) l)
  1587         ((op &::bool => bool => bool)
  1588           ((alg_prefixfree::bool list list => bool) l)
  1589           ((alg_twinfree::bool list list => bool) l)))
  1590       ((op =::bool list list => bool list list => bool)
  1591         ((alg_canon::bool list list => bool list list) l) l))"
  1592   by (import prob_canon ALG_CANON_CONSTANT)
  1593 
  1594 lemma ALG_CANON_IDEMPOT: "ALL l. alg_canon (alg_canon l) = alg_canon l"
  1595   by (import prob_canon ALG_CANON_IDEMPOT)
  1596 
  1597 lemma ALGEBRA_CANON_DEF_ALT: "ALL l. algebra_canon l = (alg_sorted l & alg_prefixfree l & alg_twinfree l)"
  1598   by (import prob_canon ALGEBRA_CANON_DEF_ALT)
  1599 
  1600 lemma ALGEBRA_CANON_BASIC: "algebra_canon [] & algebra_canon [[]] & (ALL x. algebra_canon [x])"
  1601   by (import prob_canon ALGEBRA_CANON_BASIC)
  1602 
  1603 lemma ALG_CANON_BASIC: "alg_canon [] = [] & alg_canon [[]] = [[]] & (ALL x. alg_canon [x] = [x])"
  1604   by (import prob_canon ALG_CANON_BASIC)
  1605 
  1606 lemma ALGEBRA_CANON_TL: "(All::(bool list => bool) => bool)
  1607  (%h::bool list.
  1608      (All::(bool list list => bool) => bool)
  1609       (%t::bool list list.
  1610           (op -->::bool => bool => bool)
  1611            ((algebra_canon::bool list list => bool)
  1612              ((op #::bool list => bool list list => bool list list) h t))
  1613            ((algebra_canon::bool list list => bool) t)))"
  1614   by (import prob_canon ALGEBRA_CANON_TL)
  1615 
  1616 lemma ALGEBRA_CANON_NIL_MEM: "ALL l. (algebra_canon l & [] mem l) = (l = [[]])"
  1617   by (import prob_canon ALGEBRA_CANON_NIL_MEM)
  1618 
  1619 lemma ALGEBRA_CANON_TLS: "ALL l b. algebra_canon (map (op # b) l) = algebra_canon l"
  1620   by (import prob_canon ALGEBRA_CANON_TLS)
  1621 
  1622 lemma ALGEBRA_CANON_STEP1: "(All::(bool list list => bool) => bool)
  1623  (%l1::bool list list.
  1624      (All::(bool list list => bool) => bool)
  1625       (%l2::bool list list.
  1626           (op -->::bool => bool => bool)
  1627            ((algebra_canon::bool list list => bool)
  1628              ((op @::bool list list => bool list list => bool list list)
  1629                ((map::(bool list => bool list)
  1630                       => bool list list => bool list list)
  1631                  ((op #::bool => bool list => bool list) (True::bool)) l1)
  1632                ((map::(bool list => bool list)
  1633                       => bool list list => bool list list)
  1634                  ((op #::bool => bool list => bool list) (False::bool))
  1635                  l2)))
  1636            ((op &::bool => bool => bool)
  1637              ((algebra_canon::bool list list => bool) l1)
  1638              ((algebra_canon::bool list list => bool) l2))))"
  1639   by (import prob_canon ALGEBRA_CANON_STEP1)
  1640 
  1641 lemma ALGEBRA_CANON_STEP2: "(All::(bool list list => bool) => bool)
  1642  (%l1::bool list list.
  1643      (All::(bool list list => bool) => bool)
  1644       (%l2::bool list list.
  1645           (op -->::bool => bool => bool)
  1646            ((op &::bool => bool => bool)
  1647              ((op |::bool => bool => bool)
  1648                ((Not::bool => bool)
  1649                  ((op =::bool list list => bool list list => bool) l1
  1650                    ((op #::bool list => bool list list => bool list list)
  1651                      ([]::bool list) ([]::bool list list))))
  1652                ((Not::bool => bool)
  1653                  ((op =::bool list list => bool list list => bool) l2
  1654                    ((op #::bool list => bool list list => bool list list)
  1655                      ([]::bool list) ([]::bool list list)))))
  1656              ((op &::bool => bool => bool)
  1657                ((algebra_canon::bool list list => bool) l1)
  1658                ((algebra_canon::bool list list => bool) l2)))
  1659            ((algebra_canon::bool list list => bool)
  1660              ((op @::bool list list => bool list list => bool list list)
  1661                ((map::(bool list => bool list)
  1662                       => bool list list => bool list list)
  1663                  ((op #::bool => bool list => bool list) (True::bool)) l1)
  1664                ((map::(bool list => bool list)
  1665                       => bool list list => bool list list)
  1666                  ((op #::bool => bool list => bool list) (False::bool))
  1667                  l2)))))"
  1668   by (import prob_canon ALGEBRA_CANON_STEP2)
  1669 
  1670 lemma ALGEBRA_CANON_STEP: "(All::(bool list list => bool) => bool)
  1671  (%l1::bool list list.
  1672      (All::(bool list list => bool) => bool)
  1673       (%l2::bool list list.
  1674           (op -->::bool => bool => bool)
  1675            ((op |::bool => bool => bool)
  1676              ((Not::bool => bool)
  1677                ((op =::bool list list => bool list list => bool) l1
  1678                  ((op #::bool list => bool list list => bool list list)
  1679                    ([]::bool list) ([]::bool list list))))
  1680              ((Not::bool => bool)
  1681                ((op =::bool list list => bool list list => bool) l2
  1682                  ((op #::bool list => bool list list => bool list list)
  1683                    ([]::bool list) ([]::bool list list)))))
  1684            ((op =::bool => bool => bool)
  1685              ((algebra_canon::bool list list => bool)
  1686                ((op @::bool list list => bool list list => bool list list)
  1687                  ((map::(bool list => bool list)
  1688                         => bool list list => bool list list)
  1689                    ((op #::bool => bool list => bool list) (True::bool)) l1)
  1690                  ((map::(bool list => bool list)
  1691                         => bool list list => bool list list)
  1692                    ((op #::bool => bool list => bool list) (False::bool))
  1693                    l2)))
  1694              ((op &::bool => bool => bool)
  1695                ((algebra_canon::bool list list => bool) l1)
  1696                ((algebra_canon::bool list list => bool) l2)))))"
  1697   by (import prob_canon ALGEBRA_CANON_STEP)
  1698 
  1699 lemma ALGEBRA_CANON_CASES_THM: "(All::(bool list list => bool) => bool)
  1700  (%l::bool list list.
  1701      (op -->::bool => bool => bool)
  1702       ((algebra_canon::bool list list => bool) l)
  1703       ((op |::bool => bool => bool)
  1704         ((op =::bool list list => bool list list => bool) l
  1705           ([]::bool list list))
  1706         ((op |::bool => bool => bool)
  1707           ((op =::bool list list => bool list list => bool) l
  1708             ((op #::bool list => bool list list => bool list list)
  1709               ([]::bool list) ([]::bool list list)))
  1710           ((Ex::(bool list list => bool) => bool)
  1711             (%l1::bool list list.
  1712                 (Ex::(bool list list => bool) => bool)
  1713                  (%l2::bool list list.
  1714                      (op &::bool => bool => bool)
  1715                       ((algebra_canon::bool list list => bool) l1)
  1716                       ((op &::bool => bool => bool)
  1717                         ((algebra_canon::bool list list => bool) l2)
  1718                         ((op =::bool list list => bool list list => bool) l
  1719                           ((op @::bool list list
  1720                                   => bool list list => bool list list)
  1721                             ((map::(bool list => bool list)
  1722                                    => bool list list => bool list list)
  1723                               ((op #::bool => bool list => bool list)
  1724                                 (True::bool))
  1725                               l1)
  1726                             ((map::(bool list => bool list)
  1727                                    => bool list list => bool list list)
  1728                               ((op #::bool => bool list => bool list)
  1729                                 (False::bool))
  1730                               l2))))))))))"
  1731   by (import prob_canon ALGEBRA_CANON_CASES_THM)
  1732 
  1733 lemma ALGEBRA_CANON_CASES: "(All::((bool list list => bool) => bool) => bool)
  1734  (%P::bool list list => bool.
  1735      (op -->::bool => bool => bool)
  1736       ((op &::bool => bool => bool) (P ([]::bool list list))
  1737         ((op &::bool => bool => bool)
  1738           (P ((op #::bool list => bool list list => bool list list)
  1739                ([]::bool list) ([]::bool list list)))
  1740           ((All::(bool list list => bool) => bool)
  1741             (%l1::bool list list.
  1742                 (All::(bool list list => bool) => bool)
  1743                  (%l2::bool list list.
  1744                      (op -->::bool => bool => bool)
  1745                       ((op &::bool => bool => bool)
  1746                         ((algebra_canon::bool list list => bool) l1)
  1747                         ((op &::bool => bool => bool)
  1748                           ((algebra_canon::bool list list => bool) l2)
  1749                           ((algebra_canon::bool list list => bool)
  1750                             ((op @::bool list list
  1751                                     => bool list list => bool list list)
  1752                               ((map::(bool list => bool list)
  1753                                      => bool list list => bool list list)
  1754                                 ((op #::bool => bool list => bool list)
  1755                                   (True::bool))
  1756                                 l1)
  1757                               ((map::(bool list => bool list)
  1758                                      => bool list list => bool list list)
  1759                                 ((op #::bool => bool list => bool list)
  1760                                   (False::bool))
  1761                                 l2)))))
  1762                       (P ((op @::bool list list
  1763                                  => bool list list => bool list list)
  1764                            ((map::(bool list => bool list)
  1765                                   => bool list list => bool list list)
  1766                              ((op #::bool => bool list => bool list)
  1767                                (True::bool))
  1768                              l1)
  1769                            ((map::(bool list => bool list)
  1770                                   => bool list list => bool list list)
  1771                              ((op #::bool => bool list => bool list)
  1772                                (False::bool))
  1773                              l2))))))))
  1774       ((All::(bool list list => bool) => bool)
  1775         (%l::bool list list.
  1776             (op -->::bool => bool => bool)
  1777              ((algebra_canon::bool list list => bool) l) (P l))))"
  1778   by (import prob_canon ALGEBRA_CANON_CASES)
  1779 
  1780 lemma ALGEBRA_CANON_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
  1781  (%P::bool list list => bool.
  1782      (op -->::bool => bool => bool)
  1783       ((op &::bool => bool => bool) (P ([]::bool list list))
  1784         ((op &::bool => bool => bool)
  1785           (P ((op #::bool list => bool list list => bool list list)
  1786                ([]::bool list) ([]::bool list list)))
  1787           ((All::(bool list list => bool) => bool)
  1788             (%l1::bool list list.
  1789                 (All::(bool list list => bool) => bool)
  1790                  (%l2::bool list list.
  1791                      (op -->::bool => bool => bool)
  1792                       ((op &::bool => bool => bool)
  1793                         ((algebra_canon::bool list list => bool) l1)
  1794                         ((op &::bool => bool => bool)
  1795                           ((algebra_canon::bool list list => bool) l2)
  1796                           ((op &::bool => bool => bool) (P l1)
  1797                             ((op &::bool => bool => bool) (P l2)
  1798                               ((algebra_canon::bool list list => bool)
  1799                                 ((op @::bool list list
  1800   => bool list list => bool list list)
  1801                                   ((map::(bool list => bool list)
  1802    => bool list list => bool list list)
  1803                                     ((op #::bool => bool list => bool list)
  1804 (True::bool))
  1805                                     l1)
  1806                                   ((map::(bool list => bool list)
  1807    => bool list list => bool list list)
  1808                                     ((op #::bool => bool list => bool list)
  1809 (False::bool))
  1810                                     l2)))))))
  1811                       (P ((op @::bool list list
  1812                                  => bool list list => bool list list)
  1813                            ((map::(bool list => bool list)
  1814                                   => bool list list => bool list list)
  1815                              ((op #::bool => bool list => bool list)
  1816                                (True::bool))
  1817                              l1)
  1818                            ((map::(bool list => bool list)
  1819                                   => bool list list => bool list list)
  1820                              ((op #::bool => bool list => bool list)
  1821                                (False::bool))
  1822                              l2))))))))
  1823       ((All::(bool list list => bool) => bool)
  1824         (%l::bool list list.
  1825             (op -->::bool => bool => bool)
  1826              ((algebra_canon::bool list list => bool) l) (P l))))"
  1827   by (import prob_canon ALGEBRA_CANON_INDUCTION)
  1828 
  1829 lemma MEM_NIL_STEP: "ALL l1 l2. ~ [] mem map (op # True) l1 @ map (op # False) l2"
  1830   by (import prob_canon MEM_NIL_STEP)
  1831 
  1832 lemma ALG_SORTED_PREFIXFREE_MEM_NIL: "ALL l. (alg_sorted l & alg_prefixfree l & [] mem l) = (l = [[]])"
  1833   by (import prob_canon ALG_SORTED_PREFIXFREE_MEM_NIL)
  1834 
  1835 lemma ALG_SORTED_PREFIXFREE_EQUALITY: "(All::(bool list list => bool) => bool)
  1836  (%l::bool list list.
  1837      (All::(bool list list => bool) => bool)
  1838       (%l'::bool list list.
  1839           (op -->::bool => bool => bool)
  1840            ((op &::bool => bool => bool)
  1841              ((All::(bool list => bool) => bool)
  1842                (%x::bool list.
  1843                    (op =::bool => bool => bool)
  1844                     ((op mem::bool list => bool list list => bool) x l)
  1845                     ((op mem::bool list => bool list list => bool) x l')))
  1846              ((op &::bool => bool => bool)
  1847                ((alg_sorted::bool list list => bool) l)
  1848                ((op &::bool => bool => bool)
  1849                  ((alg_sorted::bool list list => bool) l')
  1850                  ((op &::bool => bool => bool)
  1851                    ((alg_prefixfree::bool list list => bool) l)
  1852                    ((alg_prefixfree::bool list list => bool) l')))))
  1853            ((op =::bool list list => bool list list => bool) l l')))"
  1854   by (import prob_canon ALG_SORTED_PREFIXFREE_EQUALITY)
  1855 
  1856 ;end_setup
  1857 
  1858 ;setup_theory boolean_sequence
  1859 
  1860 consts
  1861   SHD :: "(nat => bool) => bool" 
  1862 
  1863 defs
  1864   SHD_primdef: "SHD == %f. f 0"
  1865 
  1866 lemma SHD_def: "ALL f. SHD f = f 0"
  1867   by (import boolean_sequence SHD_def)
  1868 
  1869 consts
  1870   STL :: "(nat => bool) => nat => bool" 
  1871 
  1872 defs
  1873   STL_primdef: "STL == %f n. f (Suc n)"
  1874 
  1875 lemma STL_def: "ALL f n. STL f n = f (Suc n)"
  1876   by (import boolean_sequence STL_def)
  1877 
  1878 consts
  1879   SCONS :: "bool => (nat => bool) => nat => bool" 
  1880 
  1881 specification (SCONS_primdef: SCONS) SCONS_def: "(ALL h t. SCONS h t 0 = h) & (ALL h t n. SCONS h t (Suc n) = t n)"
  1882   by (import boolean_sequence SCONS_def)
  1883 
  1884 consts
  1885   SDEST :: "(nat => bool) => bool * (nat => bool)" 
  1886 
  1887 defs
  1888   SDEST_primdef: "SDEST == %s. (SHD s, STL s)"
  1889 
  1890 lemma SDEST_def: "SDEST = (%s. (SHD s, STL s))"
  1891   by (import boolean_sequence SDEST_def)
  1892 
  1893 consts
  1894   SCONST :: "bool => nat => bool" 
  1895 
  1896 defs
  1897   SCONST_primdef: "SCONST == K"
  1898 
  1899 lemma SCONST_def: "SCONST = K"
  1900   by (import boolean_sequence SCONST_def)
  1901 
  1902 consts
  1903   STAKE :: "nat => (nat => bool) => bool list" 
  1904 
  1905 specification (STAKE_primdef: STAKE) STAKE_def: "(ALL s. STAKE 0 s = []) &
  1906 (ALL n s. STAKE (Suc n) s = SHD s # STAKE n (STL s))"
  1907   by (import boolean_sequence STAKE_def)
  1908 
  1909 consts
  1910   SDROP :: "nat => (nat => bool) => nat => bool" 
  1911 
  1912 specification (SDROP_primdef: SDROP) SDROP_def: "SDROP 0 = I & (ALL n. SDROP (Suc n) = SDROP n o STL)"
  1913   by (import boolean_sequence SDROP_def)
  1914 
  1915 lemma SCONS_SURJ: "ALL x. EX xa t. x = SCONS xa t"
  1916   by (import boolean_sequence SCONS_SURJ)
  1917 
  1918 lemma SHD_STL_ISO: "ALL h t. EX x. SHD x = h & STL x = t"
  1919   by (import boolean_sequence SHD_STL_ISO)
  1920 
  1921 lemma SHD_SCONS: "ALL h t. SHD (SCONS h t) = h"
  1922   by (import boolean_sequence SHD_SCONS)
  1923 
  1924 lemma STL_SCONS: "ALL h t. STL (SCONS h t) = t"
  1925   by (import boolean_sequence STL_SCONS)
  1926 
  1927 lemma SHD_SCONST: "ALL b. SHD (SCONST b) = b"
  1928   by (import boolean_sequence SHD_SCONST)
  1929 
  1930 lemma STL_SCONST: "ALL b. STL (SCONST b) = SCONST b"
  1931   by (import boolean_sequence STL_SCONST)
  1932 
  1933 ;end_setup
  1934 
  1935 ;setup_theory prob_algebra
  1936 
  1937 consts
  1938   alg_embed :: "bool list => (nat => bool) => bool" 
  1939 
  1940 specification (alg_embed_primdef: alg_embed) alg_embed_def: "(ALL s. alg_embed [] s = True) &
  1941 (ALL h t s. alg_embed (h # t) s = (h = SHD s & alg_embed t (STL s)))"
  1942   by (import prob_algebra alg_embed_def)
  1943 
  1944 consts
  1945   algebra_embed :: "bool list list => (nat => bool) => bool" 
  1946 
  1947 specification (algebra_embed_primdef: algebra_embed) algebra_embed_def: "algebra_embed [] = EMPTY &
  1948 (ALL h t.
  1949     algebra_embed (h # t) = pred_set.UNION (alg_embed h) (algebra_embed t))"
  1950   by (import prob_algebra algebra_embed_def)
  1951 
  1952 consts
  1953   measurable :: "((nat => bool) => bool) => bool" 
  1954 
  1955 defs
  1956   measurable_primdef: "measurable == %s. EX b. s = algebra_embed b"
  1957 
  1958 lemma measurable_def: "ALL s. measurable s = (EX b. s = algebra_embed b)"
  1959   by (import prob_algebra measurable_def)
  1960 
  1961 lemma HALVES_INTER: "pred_set.INTER (%x. SHD x = True) (%x. SHD x = False) = EMPTY"
  1962   by (import prob_algebra HALVES_INTER)
  1963 
  1964 lemma INTER_STL: "ALL p q. pred_set.INTER p q o STL = pred_set.INTER (p o STL) (q o STL)"
  1965   by (import prob_algebra INTER_STL)
  1966 
  1967 lemma COMPL_SHD: "ALL b. COMPL (%x. SHD x = b) = (%x. SHD x = (~ b))"
  1968   by (import prob_algebra COMPL_SHD)
  1969 
  1970 lemma ALG_EMBED_BASIC: "alg_embed [] = pred_set.UNIV &
  1971 (ALL h t.
  1972     alg_embed (h # t) = pred_set.INTER (%x. SHD x = h) (alg_embed t o STL))"
  1973   by (import prob_algebra ALG_EMBED_BASIC)
  1974 
  1975 lemma ALG_EMBED_NIL: "ALL c. All (alg_embed c) = (c = [])"
  1976   by (import prob_algebra ALG_EMBED_NIL)
  1977 
  1978 lemma ALG_EMBED_POPULATED: "ALL b. Ex (alg_embed b)"
  1979   by (import prob_algebra ALG_EMBED_POPULATED)
  1980 
  1981 lemma ALG_EMBED_PREFIX: "(All::(bool list => bool) => bool)
  1982  (%b::bool list.
  1983      (All::(bool list => bool) => bool)
  1984       (%c::bool list.
  1985           (All::((nat => bool) => bool) => bool)
  1986            (%s::nat => bool.
  1987                (op -->::bool => bool => bool)
  1988                 ((op &::bool => bool => bool)
  1989                   ((alg_embed::bool list => (nat => bool) => bool) b s)
  1990                   ((alg_embed::bool list => (nat => bool) => bool) c s))
  1991                 ((op |::bool => bool => bool)
  1992                   ((IS_PREFIX::bool list => bool list => bool) b c)
  1993                   ((IS_PREFIX::bool list => bool list => bool) c b)))))"
  1994   by (import prob_algebra ALG_EMBED_PREFIX)
  1995 
  1996 lemma ALG_EMBED_PREFIX_SUBSET: "ALL b c. SUBSET (alg_embed b) (alg_embed c) = IS_PREFIX b c"
  1997   by (import prob_algebra ALG_EMBED_PREFIX_SUBSET)
  1998 
  1999 lemma ALG_EMBED_TWINS: "ALL l.
  2000    pred_set.UNION (alg_embed (SNOC True l)) (alg_embed (SNOC False l)) =
  2001    alg_embed l"
  2002   by (import prob_algebra ALG_EMBED_TWINS)
  2003 
  2004 lemma ALGEBRA_EMBED_BASIC: "algebra_embed [] = EMPTY &
  2005 algebra_embed [[]] = pred_set.UNIV &
  2006 (ALL b. algebra_embed [[b]] = (%s. SHD s = b))"
  2007   by (import prob_algebra ALGEBRA_EMBED_BASIC)
  2008 
  2009 lemma ALGEBRA_EMBED_MEM: "(All::(bool list list => bool) => bool)
  2010  (%b::bool list list.
  2011      (All::((nat => bool) => bool) => bool)
  2012       (%x::nat => bool.
  2013           (op -->::bool => bool => bool)
  2014            ((algebra_embed::bool list list => (nat => bool) => bool) b x)
  2015            ((Ex::(bool list => bool) => bool)
  2016              (%l::bool list.
  2017                  (op &::bool => bool => bool)
  2018                   ((op mem::bool list => bool list list => bool) l b)
  2019                   ((alg_embed::bool list => (nat => bool) => bool) l x)))))"
  2020   by (import prob_algebra ALGEBRA_EMBED_MEM)
  2021 
  2022 lemma ALGEBRA_EMBED_APPEND: "ALL l1 l2.
  2023    algebra_embed (l1 @ l2) =
  2024    pred_set.UNION (algebra_embed l1) (algebra_embed l2)"
  2025   by (import prob_algebra ALGEBRA_EMBED_APPEND)
  2026 
  2027 lemma ALGEBRA_EMBED_TLS: "ALL l b.
  2028    algebra_embed (map (op # b) l) (SCONS h t) = (h = b & algebra_embed l t)"
  2029   by (import prob_algebra ALGEBRA_EMBED_TLS)
  2030 
  2031 lemma ALG_CANON_PREFS_EMBED: "ALL l b. algebra_embed (alg_canon_prefs l b) = algebra_embed (l # b)"
  2032   by (import prob_algebra ALG_CANON_PREFS_EMBED)
  2033 
  2034 lemma ALG_CANON_FIND_EMBED: "ALL l b. algebra_embed (alg_canon_find l b) = algebra_embed (l # b)"
  2035   by (import prob_algebra ALG_CANON_FIND_EMBED)
  2036 
  2037 lemma ALG_CANON1_EMBED: "ALL x. algebra_embed (alg_canon1 x) = algebra_embed x"
  2038   by (import prob_algebra ALG_CANON1_EMBED)
  2039 
  2040 lemma ALG_CANON_MERGE_EMBED: "ALL l b. algebra_embed (alg_canon_merge l b) = algebra_embed (l # b)"
  2041   by (import prob_algebra ALG_CANON_MERGE_EMBED)
  2042 
  2043 lemma ALG_CANON2_EMBED: "ALL x. algebra_embed (alg_canon2 x) = algebra_embed x"
  2044   by (import prob_algebra ALG_CANON2_EMBED)
  2045 
  2046 lemma ALG_CANON_EMBED: "ALL l. algebra_embed (alg_canon l) = algebra_embed l"
  2047   by (import prob_algebra ALG_CANON_EMBED)
  2048 
  2049 lemma ALGEBRA_CANON_UNIV: "(All::(bool list list => bool) => bool)
  2050  (%l::bool list list.
  2051      (op -->::bool => bool => bool)
  2052       ((algebra_canon::bool list list => bool) l)
  2053       ((op -->::bool => bool => bool)
  2054         ((op =::((nat => bool) => bool) => ((nat => bool) => bool) => bool)
  2055           ((algebra_embed::bool list list => (nat => bool) => bool) l)
  2056           (pred_set.UNIV::(nat => bool) => bool))
  2057         ((op =::bool list list => bool list list => bool) l
  2058           ((op #::bool list => bool list list => bool list list)
  2059             ([]::bool list) ([]::bool list list)))))"
  2060   by (import prob_algebra ALGEBRA_CANON_UNIV)
  2061 
  2062 lemma ALG_CANON_REP: "ALL b c. (alg_canon b = alg_canon c) = (algebra_embed b = algebra_embed c)"
  2063   by (import prob_algebra ALG_CANON_REP)
  2064 
  2065 lemma ALGEBRA_CANON_EMBED_EMPTY: "(All::(bool list list => bool) => bool)
  2066  (%l::bool list list.
  2067      (op -->::bool => bool => bool)
  2068       ((algebra_canon::bool list list => bool) l)
  2069       ((op =::bool => bool => bool)
  2070         ((All::((nat => bool) => bool) => bool)
  2071           (%v::nat => bool.
  2072               (Not::bool => bool)
  2073                ((algebra_embed::bool list list => (nat => bool) => bool) l
  2074                  v)))
  2075         ((op =::bool list list => bool list list => bool) l
  2076           ([]::bool list list))))"
  2077   by (import prob_algebra ALGEBRA_CANON_EMBED_EMPTY)
  2078 
  2079 lemma ALGEBRA_CANON_EMBED_UNIV: "(All::(bool list list => bool) => bool)
  2080  (%l::bool list list.
  2081      (op -->::bool => bool => bool)
  2082       ((algebra_canon::bool list list => bool) l)
  2083       ((op =::bool => bool => bool)
  2084         ((All::((nat => bool) => bool) => bool)
  2085           ((algebra_embed::bool list list => (nat => bool) => bool) l))
  2086         ((op =::bool list list => bool list list => bool) l
  2087           ((op #::bool list => bool list list => bool list list)
  2088             ([]::bool list) ([]::bool list list)))))"
  2089   by (import prob_algebra ALGEBRA_CANON_EMBED_UNIV)
  2090 
  2091 lemma MEASURABLE_ALGEBRA: "ALL b. measurable (algebra_embed b)"
  2092   by (import prob_algebra MEASURABLE_ALGEBRA)
  2093 
  2094 lemma MEASURABLE_BASIC: "measurable EMPTY &
  2095 measurable pred_set.UNIV & (ALL b. measurable (%s. SHD s = b))"
  2096   by (import prob_algebra MEASURABLE_BASIC)
  2097 
  2098 lemma MEASURABLE_SHD: "ALL b. measurable (%s. SHD s = b)"
  2099   by (import prob_algebra MEASURABLE_SHD)
  2100 
  2101 lemma ALGEBRA_EMBED_COMPL: "ALL l. EX l'. COMPL (algebra_embed l) = algebra_embed l'"
  2102   by (import prob_algebra ALGEBRA_EMBED_COMPL)
  2103 
  2104 lemma MEASURABLE_COMPL: "ALL s. measurable (COMPL s) = measurable s"
  2105   by (import prob_algebra MEASURABLE_COMPL)
  2106 
  2107 lemma MEASURABLE_UNION: "(All::(((nat => bool) => bool) => bool) => bool)
  2108  (%s::(nat => bool) => bool.
  2109      (All::(((nat => bool) => bool) => bool) => bool)
  2110       (%t::(nat => bool) => bool.
  2111           (op -->::bool => bool => bool)
  2112            ((op &::bool => bool => bool)
  2113              ((measurable::((nat => bool) => bool) => bool) s)
  2114              ((measurable::((nat => bool) => bool) => bool) t))
  2115            ((measurable::((nat => bool) => bool) => bool)
  2116              ((pred_set.UNION::((nat => bool) => bool)
  2117                                => ((nat => bool) => bool)
  2118                                   => (nat => bool) => bool)
  2119                s t))))"
  2120   by (import prob_algebra MEASURABLE_UNION)
  2121 
  2122 lemma MEASURABLE_INTER: "(All::(((nat => bool) => bool) => bool) => bool)
  2123  (%s::(nat => bool) => bool.
  2124      (All::(((nat => bool) => bool) => bool) => bool)
  2125       (%t::(nat => bool) => bool.
  2126           (op -->::bool => bool => bool)
  2127            ((op &::bool => bool => bool)
  2128              ((measurable::((nat => bool) => bool) => bool) s)
  2129              ((measurable::((nat => bool) => bool) => bool) t))
  2130            ((measurable::((nat => bool) => bool) => bool)
  2131              ((pred_set.INTER::((nat => bool) => bool)
  2132                                => ((nat => bool) => bool)
  2133                                   => (nat => bool) => bool)
  2134                s t))))"
  2135   by (import prob_algebra MEASURABLE_INTER)
  2136 
  2137 lemma MEASURABLE_STL: "ALL p. measurable (p o STL) = measurable p"
  2138   by (import prob_algebra MEASURABLE_STL)
  2139 
  2140 lemma MEASURABLE_SDROP: "ALL n p. measurable (p o SDROP n) = measurable p"
  2141   by (import prob_algebra MEASURABLE_SDROP)
  2142 
  2143 lemma MEASURABLE_INTER_HALVES: "ALL p.
  2144    (measurable (pred_set.INTER (%x. SHD x = True) p) &
  2145     measurable (pred_set.INTER (%x. SHD x = False) p)) =
  2146    measurable p"
  2147   by (import prob_algebra MEASURABLE_INTER_HALVES)
  2148 
  2149 lemma MEASURABLE_HALVES: "ALL p q.
  2150    measurable
  2151     (pred_set.UNION (pred_set.INTER (%x. SHD x = True) p)
  2152       (pred_set.INTER (%x. SHD x = False) q)) =
  2153    (measurable (pred_set.INTER (%x. SHD x = True) p) &
  2154     measurable (pred_set.INTER (%x. SHD x = False) q))"
  2155   by (import prob_algebra MEASURABLE_HALVES)
  2156 
  2157 lemma MEASURABLE_INTER_SHD: "ALL b p.
  2158    measurable (pred_set.INTER (%x. SHD x = b) (p o STL)) = measurable p"
  2159   by (import prob_algebra MEASURABLE_INTER_SHD)
  2160 
  2161 ;end_setup
  2162 
  2163 ;setup_theory prob
  2164 
  2165 consts
  2166   alg_measure :: "bool list list => real" 
  2167 
  2168 specification (alg_measure_primdef: alg_measure) alg_measure_def: "alg_measure [] = 0 &
  2169 (ALL l rest. alg_measure (l # rest) = (1 / 2) ^ length l + alg_measure rest)"
  2170   by (import prob alg_measure_def)
  2171 
  2172 consts
  2173   algebra_measure :: "bool list list => real" 
  2174 
  2175 defs
  2176   algebra_measure_primdef: "algebra_measure ==
  2177 %b. inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
  2178 
  2179 lemma algebra_measure_def: "ALL b.
  2180    algebra_measure b =
  2181    inf (%r. EX c. algebra_embed b = algebra_embed c & alg_measure c = r)"
  2182   by (import prob algebra_measure_def)
  2183 
  2184 consts
  2185   prob :: "((nat => bool) => bool) => real" 
  2186 
  2187 defs
  2188   prob_primdef: "prob ==
  2189 %s. sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
  2190 
  2191 lemma prob_def: "ALL s.
  2192    prob s =
  2193    sup (%r. EX b. algebra_measure b = r & SUBSET (algebra_embed b) s)"
  2194   by (import prob prob_def)
  2195 
  2196 lemma ALG_TWINS_MEASURE: "ALL l::bool list.
  2197    ((1::real) / (2::real)) ^ length (SNOC True l) +
  2198    ((1::real) / (2::real)) ^ length (SNOC False l) =
  2199    ((1::real) / (2::real)) ^ length l"
  2200   by (import prob ALG_TWINS_MEASURE)
  2201 
  2202 lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 &
  2203 alg_measure [[]] = 1 & (ALL b. alg_measure [[b]] = 1 / 2)"
  2204   by (import prob ALG_MEASURE_BASIC)
  2205 
  2206 lemma ALG_MEASURE_POS: "ALL l. 0 <= alg_measure l"
  2207   by (import prob ALG_MEASURE_POS)
  2208 
  2209 lemma ALG_MEASURE_APPEND: "ALL l1 l2. alg_measure (l1 @ l2) = alg_measure l1 + alg_measure l2"
  2210   by (import prob ALG_MEASURE_APPEND)
  2211 
  2212 lemma ALG_MEASURE_TLS: "ALL l b. 2 * alg_measure (map (op # b) l) = alg_measure l"
  2213   by (import prob ALG_MEASURE_TLS)
  2214 
  2215 lemma ALG_CANON_PREFS_MONO: "ALL l b. alg_measure (alg_canon_prefs l b) <= alg_measure (l # b)"
  2216   by (import prob ALG_CANON_PREFS_MONO)
  2217 
  2218 lemma ALG_CANON_FIND_MONO: "ALL l b. alg_measure (alg_canon_find l b) <= alg_measure (l # b)"
  2219   by (import prob ALG_CANON_FIND_MONO)
  2220 
  2221 lemma ALG_CANON1_MONO: "ALL x. alg_measure (alg_canon1 x) <= alg_measure x"
  2222   by (import prob ALG_CANON1_MONO)
  2223 
  2224 lemma ALG_CANON_MERGE_MONO: "ALL l b. alg_measure (alg_canon_merge l b) <= alg_measure (l # b)"
  2225   by (import prob ALG_CANON_MERGE_MONO)
  2226 
  2227 lemma ALG_CANON2_MONO: "ALL x. alg_measure (alg_canon2 x) <= alg_measure x"
  2228   by (import prob ALG_CANON2_MONO)
  2229 
  2230 lemma ALG_CANON_MONO: "ALL l. alg_measure (alg_canon l) <= alg_measure l"
  2231   by (import prob ALG_CANON_MONO)
  2232 
  2233 lemma ALGEBRA_MEASURE_DEF_ALT: "ALL l. algebra_measure l = alg_measure (alg_canon l)"
  2234   by (import prob ALGEBRA_MEASURE_DEF_ALT)
  2235 
  2236 lemma ALGEBRA_MEASURE_BASIC: "algebra_measure [] = 0 &
  2237 algebra_measure [[]] = 1 & (ALL b. algebra_measure [[b]] = 1 / 2)"
  2238   by (import prob ALGEBRA_MEASURE_BASIC)
  2239 
  2240 lemma ALGEBRA_CANON_MEASURE_MAX: "(All::(bool list list => bool) => bool)
  2241  (%l::bool list list.
  2242      (op -->::bool => bool => bool)
  2243       ((algebra_canon::bool list list => bool) l)
  2244       ((op <=::real => real => bool)
  2245         ((alg_measure::bool list list => real) l) (1::real)))"
  2246   by (import prob ALGEBRA_CANON_MEASURE_MAX)
  2247 
  2248 lemma ALGEBRA_MEASURE_MAX: "ALL l. algebra_measure l <= 1"
  2249   by (import prob ALGEBRA_MEASURE_MAX)
  2250 
  2251 lemma ALGEBRA_MEASURE_MONO_EMBED: "(All::(bool list list => bool) => bool)
  2252  (%x::bool list list.
  2253      (All::(bool list list => bool) => bool)
  2254       (%xa::bool list list.
  2255           (op -->::bool => bool => bool)
  2256            ((SUBSET::((nat => bool) => bool)
  2257                      => ((nat => bool) => bool) => bool)
  2258              ((algebra_embed::bool list list => (nat => bool) => bool) x)
  2259              ((algebra_embed::bool list list => (nat => bool) => bool) xa))
  2260            ((op <=::real => real => bool)
  2261              ((algebra_measure::bool list list => real) x)
  2262              ((algebra_measure::bool list list => real) xa))))"
  2263   by (import prob ALGEBRA_MEASURE_MONO_EMBED)
  2264 
  2265 lemma ALG_MEASURE_COMPL: "(All::(bool list list => bool) => bool)
  2266  (%l::bool list list.
  2267      (op -->::bool => bool => bool)
  2268       ((algebra_canon::bool list list => bool) l)
  2269       ((All::(bool list list => bool) => bool)
  2270         (%c::bool list list.
  2271             (op -->::bool => bool => bool)
  2272              ((algebra_canon::bool list list => bool) c)
  2273              ((op -->::bool => bool => bool)
  2274                ((op =::((nat => bool) => bool)
  2275                        => ((nat => bool) => bool) => bool)
  2276                  ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
  2277                    ((algebra_embed::bool list list => (nat => bool) => bool)
  2278                      l))
  2279                  ((algebra_embed::bool list list => (nat => bool) => bool)
  2280                    c))
  2281                ((op =::real => real => bool)
  2282                  ((op +::real => real => real)
  2283                    ((alg_measure::bool list list => real) l)
  2284                    ((alg_measure::bool list list => real) c))
  2285                  (1::real))))))"
  2286   by (import prob ALG_MEASURE_COMPL)
  2287 
  2288 lemma ALG_MEASURE_ADDITIVE: "(All::(bool list list => bool) => bool)
  2289  (%l::bool list list.
  2290      (op -->::bool => bool => bool)
  2291       ((algebra_canon::bool list list => bool) l)
  2292       ((All::(bool list list => bool) => bool)
  2293         (%c::bool list list.
  2294             (op -->::bool => bool => bool)
  2295              ((algebra_canon::bool list list => bool) c)
  2296              ((All::(bool list list => bool) => bool)
  2297                (%d::bool list list.
  2298                    (op -->::bool => bool => bool)
  2299                     ((algebra_canon::bool list list => bool) d)
  2300                     ((op -->::bool => bool => bool)
  2301                       ((op &::bool => bool => bool)
  2302                         ((op =::((nat => bool) => bool)
  2303                                 => ((nat => bool) => bool) => bool)
  2304                           ((pred_set.INTER::((nat => bool) => bool)
  2305       => ((nat => bool) => bool) => (nat => bool) => bool)
  2306                             ((algebra_embed::bool list list
  2307        => (nat => bool) => bool)
  2308                               c)
  2309                             ((algebra_embed::bool list list
  2310        => (nat => bool) => bool)
  2311                               d))
  2312                           (EMPTY::(nat => bool) => bool))
  2313                         ((op =::((nat => bool) => bool)
  2314                                 => ((nat => bool) => bool) => bool)
  2315                           ((algebra_embed::bool list list
  2316      => (nat => bool) => bool)
  2317                             l)
  2318                           ((pred_set.UNION::((nat => bool) => bool)
  2319       => ((nat => bool) => bool) => (nat => bool) => bool)
  2320                             ((algebra_embed::bool list list
  2321        => (nat => bool) => bool)
  2322                               c)
  2323                             ((algebra_embed::bool list list
  2324        => (nat => bool) => bool)
  2325                               d))))
  2326                       ((op =::real => real => bool)
  2327                         ((alg_measure::bool list list => real) l)
  2328                         ((op +::real => real => real)
  2329                           ((alg_measure::bool list list => real) c)
  2330                           ((alg_measure::bool list list => real) d)))))))))"
  2331   by (import prob ALG_MEASURE_ADDITIVE)
  2332 
  2333 lemma PROB_ALGEBRA: "ALL l. prob (algebra_embed l) = algebra_measure l"
  2334   by (import prob PROB_ALGEBRA)
  2335 
  2336 lemma PROB_BASIC: "prob EMPTY = 0 &
  2337 prob pred_set.UNIV = 1 & (ALL b. prob (%s. SHD s = b) = 1 / 2)"
  2338   by (import prob PROB_BASIC)
  2339 
  2340 lemma PROB_ADDITIVE: "(All::(((nat => bool) => bool) => bool) => bool)
  2341  (%s::(nat => bool) => bool.
  2342      (All::(((nat => bool) => bool) => bool) => bool)
  2343       (%t::(nat => bool) => bool.
  2344           (op -->::bool => bool => bool)
  2345            ((op &::bool => bool => bool)
  2346              ((measurable::((nat => bool) => bool) => bool) s)
  2347              ((op &::bool => bool => bool)
  2348                ((measurable::((nat => bool) => bool) => bool) t)
  2349                ((op =::((nat => bool) => bool)
  2350                        => ((nat => bool) => bool) => bool)
  2351                  ((pred_set.INTER::((nat => bool) => bool)
  2352                                    => ((nat => bool) => bool)
  2353 => (nat => bool) => bool)
  2354                    s t)
  2355                  (EMPTY::(nat => bool) => bool))))
  2356            ((op =::real => real => bool)
  2357              ((prob::((nat => bool) => bool) => real)
  2358                ((pred_set.UNION::((nat => bool) => bool)
  2359                                  => ((nat => bool) => bool)
  2360                                     => (nat => bool) => bool)
  2361                  s t))
  2362              ((op +::real => real => real)
  2363                ((prob::((nat => bool) => bool) => real) s)
  2364                ((prob::((nat => bool) => bool) => real) t)))))"
  2365   by (import prob PROB_ADDITIVE)
  2366 
  2367 lemma PROB_COMPL: "(All::(((nat => bool) => bool) => bool) => bool)
  2368  (%s::(nat => bool) => bool.
  2369      (op -->::bool => bool => bool)
  2370       ((measurable::((nat => bool) => bool) => bool) s)
  2371       ((op =::real => real => bool)
  2372         ((prob::((nat => bool) => bool) => real)
  2373           ((COMPL::((nat => bool) => bool) => (nat => bool) => bool) s))
  2374         ((op -::real => real => real) (1::real)
  2375           ((prob::((nat => bool) => bool) => real) s))))"
  2376   by (import prob PROB_COMPL)
  2377 
  2378 lemma PROB_SUP_EXISTS1: "ALL s. EX x b. algebra_measure b = x & SUBSET (algebra_embed b) s"
  2379   by (import prob PROB_SUP_EXISTS1)
  2380 
  2381 lemma PROB_SUP_EXISTS2: "(All::(((nat => bool) => bool) => bool) => bool)
  2382  (%s::(nat => bool) => bool.
  2383      (Ex::(real => bool) => bool)
  2384       (%x::real.
  2385           (All::(real => bool) => bool)
  2386            (%r::real.
  2387                (op -->::bool => bool => bool)
  2388                 ((Ex::(bool list list => bool) => bool)
  2389                   (%b::bool list list.
  2390                       (op &::bool => bool => bool)
  2391                        ((op =::real => real => bool)
  2392                          ((algebra_measure::bool list list => real) b) r)
  2393                        ((SUBSET::((nat => bool) => bool)
  2394                                  => ((nat => bool) => bool) => bool)
  2395                          ((algebra_embed::bool list list
  2396     => (nat => bool) => bool)
  2397                            b)
  2398                          s)))
  2399                 ((op <=::real => real => bool) r x))))"
  2400   by (import prob PROB_SUP_EXISTS2)
  2401 
  2402 lemma PROB_LE_X: "(All::(((nat => bool) => bool) => bool) => bool)
  2403  (%s::(nat => bool) => bool.
  2404      (All::(real => bool) => bool)
  2405       (%x::real.
  2406           (op -->::bool => bool => bool)
  2407            ((All::(((nat => bool) => bool) => bool) => bool)
  2408              (%s'::(nat => bool) => bool.
  2409                  (op -->::bool => bool => bool)
  2410                   ((op &::bool => bool => bool)
  2411                     ((measurable::((nat => bool) => bool) => bool) s')
  2412                     ((SUBSET::((nat => bool) => bool)
  2413                               => ((nat => bool) => bool) => bool)
  2414                       s' s))
  2415                   ((op <=::real => real => bool)
  2416                     ((prob::((nat => bool) => bool) => real) s') x)))
  2417            ((op <=::real => real => bool)
  2418              ((prob::((nat => bool) => bool) => real) s) x)))"
  2419   by (import prob PROB_LE_X)
  2420 
  2421 lemma X_LE_PROB: "(All::(((nat => bool) => bool) => bool) => bool)
  2422  (%s::(nat => bool) => bool.
  2423      (All::(real => bool) => bool)
  2424       (%x::real.
  2425           (op -->::bool => bool => bool)
  2426            ((Ex::(((nat => bool) => bool) => bool) => bool)
  2427              (%s'::(nat => bool) => bool.
  2428                  (op &::bool => bool => bool)
  2429                   ((measurable::((nat => bool) => bool) => bool) s')
  2430                   ((op &::bool => bool => bool)
  2431                     ((SUBSET::((nat => bool) => bool)
  2432                               => ((nat => bool) => bool) => bool)
  2433                       s' s)
  2434                     ((op <=::real => real => bool) x
  2435                       ((prob::((nat => bool) => bool) => real) s')))))
  2436            ((op <=::real => real => bool) x
  2437              ((prob::((nat => bool) => bool) => real) s))))"
  2438   by (import prob X_LE_PROB)
  2439 
  2440 lemma PROB_SUBSET_MONO: "(All::(((nat => bool) => bool) => bool) => bool)
  2441  (%s::(nat => bool) => bool.
  2442      (All::(((nat => bool) => bool) => bool) => bool)
  2443       (%t::(nat => bool) => bool.
  2444           (op -->::bool => bool => bool)
  2445            ((SUBSET::((nat => bool) => bool)
  2446                      => ((nat => bool) => bool) => bool)
  2447              s t)
  2448            ((op <=::real => real => bool)
  2449              ((prob::((nat => bool) => bool) => real) s)
  2450              ((prob::((nat => bool) => bool) => real) t))))"
  2451   by (import prob PROB_SUBSET_MONO)
  2452 
  2453 lemma PROB_ALG: "ALL x. prob (alg_embed x) = (1 / 2) ^ length x"
  2454   by (import prob PROB_ALG)
  2455 
  2456 lemma PROB_STL: "(All::(((nat => bool) => bool) => bool) => bool)
  2457  (%p::(nat => bool) => bool.
  2458      (op -->::bool => bool => bool)
  2459       ((measurable::((nat => bool) => bool) => bool) p)
  2460       ((op =::real => real => bool)
  2461         ((prob::((nat => bool) => bool) => real)
  2462           ((op o::((nat => bool) => bool)
  2463                   => ((nat => bool) => nat => bool)
  2464                      => (nat => bool) => bool)
  2465             p (STL::(nat => bool) => nat => bool)))
  2466         ((prob::((nat => bool) => bool) => real) p)))"
  2467   by (import prob PROB_STL)
  2468 
  2469 lemma PROB_SDROP: "(All::(nat => bool) => bool)
  2470  (%n::nat.
  2471      (All::(((nat => bool) => bool) => bool) => bool)
  2472       (%p::(nat => bool) => bool.
  2473           (op -->::bool => bool => bool)
  2474            ((measurable::((nat => bool) => bool) => bool) p)
  2475            ((op =::real => real => bool)
  2476              ((prob::((nat => bool) => bool) => real)
  2477                ((op o::((nat => bool) => bool)
  2478                        => ((nat => bool) => nat => bool)
  2479                           => (nat => bool) => bool)
  2480                  p ((SDROP::nat => (nat => bool) => nat => bool) n)))
  2481              ((prob::((nat => bool) => bool) => real) p))))"
  2482   by (import prob PROB_SDROP)
  2483 
  2484 lemma PROB_INTER_HALVES: "(All::(((nat => bool) => bool) => bool) => bool)
  2485  (%p::(nat => bool) => bool.
  2486      (op -->::bool => bool => bool)
  2487       ((measurable::((nat => bool) => bool) => bool) p)
  2488       ((op =::real => real => bool)
  2489         ((op +::real => real => real)
  2490           ((prob::((nat => bool) => bool) => real)
  2491             ((pred_set.INTER::((nat => bool) => bool)
  2492                               => ((nat => bool) => bool)
  2493                                  => (nat => bool) => bool)
  2494               (%x::nat => bool.
  2495                   (op =::bool => bool => bool)
  2496                    ((SHD::(nat => bool) => bool) x) (True::bool))
  2497               p))
  2498           ((prob::((nat => bool) => bool) => real)
  2499             ((pred_set.INTER::((nat => bool) => bool)
  2500                               => ((nat => bool) => bool)
  2501                                  => (nat => bool) => bool)
  2502               (%x::nat => bool.
  2503                   (op =::bool => bool => bool)
  2504                    ((SHD::(nat => bool) => bool) x) (False::bool))
  2505               p)))
  2506         ((prob::((nat => bool) => bool) => real) p)))"
  2507   by (import prob PROB_INTER_HALVES)
  2508 
  2509 lemma PROB_INTER_SHD: "(All::(bool => bool) => bool)
  2510  (%b::bool.
  2511      (All::(((nat => bool) => bool) => bool) => bool)
  2512       (%p::(nat => bool) => bool.
  2513           (op -->::bool => bool => bool)
  2514            ((measurable::((nat => bool) => bool) => bool) p)
  2515            ((op =::real => real => bool)
  2516              ((prob::((nat => bool) => bool) => real)
  2517                ((pred_set.INTER::((nat => bool) => bool)
  2518                                  => ((nat => bool) => bool)
  2519                                     => (nat => bool) => bool)
  2520                  (%x::nat => bool.
  2521                      (op =::bool => bool => bool)
  2522                       ((SHD::(nat => bool) => bool) x) b)
  2523                  ((op o::((nat => bool) => bool)
  2524                          => ((nat => bool) => nat => bool)
  2525                             => (nat => bool) => bool)
  2526                    p (STL::(nat => bool) => nat => bool))))
  2527              ((op *::real => real => real)
  2528                ((op /::real => real => real) (1::real)
  2529                  ((number_of::bin => real)
  2530                    ((op BIT::bin => bool => bin)
  2531                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  2532                        (True::bool))
  2533                      (False::bool))))
  2534                ((prob::((nat => bool) => bool) => real) p)))))"
  2535   by (import prob PROB_INTER_SHD)
  2536 
  2537 lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l"
  2538   by (import prob ALGEBRA_MEASURE_POS)
  2539 
  2540 lemma ALGEBRA_MEASURE_RANGE: "ALL l. 0 <= algebra_measure l & algebra_measure l <= 1"
  2541   by (import prob ALGEBRA_MEASURE_RANGE)
  2542 
  2543 lemma PROB_POS: "ALL p. 0 <= prob p"
  2544   by (import prob PROB_POS)
  2545 
  2546 lemma PROB_MAX: "ALL p. prob p <= 1"
  2547   by (import prob PROB_MAX)
  2548 
  2549 lemma PROB_RANGE: "ALL p. 0 <= prob p & prob p <= 1"
  2550   by (import prob PROB_RANGE)
  2551 
  2552 lemma ABS_PROB: "ALL p. abs (prob p) = prob p"
  2553   by (import prob ABS_PROB)
  2554 
  2555 lemma PROB_SHD: "ALL b. prob (%s. SHD s = b) = 1 / 2"
  2556   by (import prob PROB_SHD)
  2557 
  2558 lemma PROB_COMPL_LE1: "(All::(((nat => bool) => bool) => bool) => bool)
  2559  (%p::(nat => bool) => bool.
  2560      (All::(real => bool) => bool)
  2561       (%r::real.
  2562           (op -->::bool => bool => bool)
  2563            ((measurable::((nat => bool) => bool) => bool) p)
  2564            ((op =::bool => bool => bool)
  2565              ((op <=::real => real => bool)
  2566                ((prob::((nat => bool) => bool) => real)
  2567                  ((COMPL::((nat => bool) => bool) => (nat => bool) => bool)
  2568                    p))
  2569                r)
  2570              ((op <=::real => real => bool)
  2571                ((op -::real => real => real) (1::real) r)
  2572                ((prob::((nat => bool) => bool) => real) p)))))"
  2573   by (import prob PROB_COMPL_LE1)
  2574 
  2575 ;end_setup
  2576 
  2577 ;setup_theory prob_pseudo
  2578 
  2579 consts
  2580   pseudo_linear_hd :: "nat => bool" 
  2581 
  2582 defs
  2583   pseudo_linear_hd_primdef: "pseudo_linear_hd == EVEN"
  2584 
  2585 lemma pseudo_linear_hd_def: "pseudo_linear_hd = EVEN"
  2586   by (import prob_pseudo pseudo_linear_hd_def)
  2587 
  2588 consts
  2589   pseudo_linear_tl :: "nat => nat => nat => nat => nat" 
  2590 
  2591 defs
  2592   pseudo_linear_tl_primdef: "pseudo_linear_tl == %a b n x. (a * x + b) mod (2 * n + 1)"
  2593 
  2594 lemma pseudo_linear_tl_def: "ALL a b n x. pseudo_linear_tl a b n x = (a * x + b) mod (2 * n + 1)"
  2595   by (import prob_pseudo pseudo_linear_tl_def)
  2596 
  2597 lemma PSEUDO_LINEAR1_EXECUTE: "EX x. (ALL xa. SHD (x xa) = pseudo_linear_hd xa) &
  2598       (ALL xa.
  2599           STL (x xa) =
  2600           x (pseudo_linear_tl
  2601               (NUMERAL
  2602                 (NUMERAL_BIT1
  2603                   (NUMERAL_BIT1
  2604                     (NUMERAL_BIT1
  2605                       (NUMERAL_BIT2
  2606                         (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  2607               (NUMERAL
  2608                 (NUMERAL_BIT1
  2609                   (NUMERAL_BIT1
  2610                     (NUMERAL_BIT1
  2611                       (NUMERAL_BIT1
  2612                         (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  2613               (NUMERAL
  2614                 (NUMERAL_BIT1
  2615                   (NUMERAL_BIT1
  2616                     (NUMERAL_BIT1
  2617                       (NUMERAL_BIT1
  2618                         (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  2619               xa))"
  2620   by (import prob_pseudo PSEUDO_LINEAR1_EXECUTE)
  2621 
  2622 consts
  2623   pseudo_linear1 :: "nat => nat => bool" 
  2624 
  2625 specification (pseudo_linear1_primdef: pseudo_linear1) pseudo_linear1_def: "(ALL x. SHD (pseudo_linear1 x) = pseudo_linear_hd x) &
  2626 (ALL x.
  2627     STL (pseudo_linear1 x) =
  2628     pseudo_linear1
  2629      (pseudo_linear_tl
  2630        (NUMERAL
  2631          (NUMERAL_BIT1
  2632            (NUMERAL_BIT1
  2633              (NUMERAL_BIT1
  2634                (NUMERAL_BIT2 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  2635        (NUMERAL
  2636          (NUMERAL_BIT1
  2637            (NUMERAL_BIT1
  2638              (NUMERAL_BIT1
  2639                (NUMERAL_BIT1 (NUMERAL_BIT1 (NUMERAL_BIT2 ALT_ZERO)))))))
  2640        (NUMERAL
  2641          (NUMERAL_BIT1
  2642            (NUMERAL_BIT1
  2643              (NUMERAL_BIT1
  2644                (NUMERAL_BIT1 (NUMERAL_BIT2 (NUMERAL_BIT1 ALT_ZERO)))))))
  2645        x))"
  2646   by (import prob_pseudo pseudo_linear1_def)
  2647 
  2648 consts
  2649   pseudo :: "nat => nat => bool" 
  2650 
  2651 defs
  2652   pseudo_primdef: "pseudo == pseudo_linear1"
  2653 
  2654 lemma pseudo_def: "pseudo = pseudo_linear1"
  2655   by (import prob_pseudo pseudo_def)
  2656 
  2657 ;end_setup
  2658 
  2659 ;setup_theory prob_indep
  2660 
  2661 consts
  2662   indep_set :: "((nat => bool) => bool) => ((nat => bool) => bool) => bool" 
  2663 
  2664 defs
  2665   indep_set_primdef: "indep_set ==
  2666 %p q. measurable p &
  2667       measurable q & prob (pred_set.INTER p q) = prob p * prob q"
  2668 
  2669 lemma indep_set_def: "ALL p q.
  2670    indep_set p q =
  2671    (measurable p &
  2672     measurable q & prob (pred_set.INTER p q) = prob p * prob q)"
  2673   by (import prob_indep indep_set_def)
  2674 
  2675 consts
  2676   alg_cover_set :: "bool list list => bool" 
  2677 
  2678 defs
  2679   alg_cover_set_primdef: "alg_cover_set ==
  2680 %l. alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV"
  2681 
  2682 lemma alg_cover_set_def: "ALL l.
  2683    alg_cover_set l =
  2684    (alg_sorted l & alg_prefixfree l & algebra_embed l = pred_set.UNIV)"
  2685   by (import prob_indep alg_cover_set_def)
  2686 
  2687 consts
  2688   alg_cover :: "bool list list => (nat => bool) => bool list" 
  2689 
  2690 defs
  2691   alg_cover_primdef: "alg_cover == %l x. SOME b. b mem l & alg_embed b x"
  2692 
  2693 lemma alg_cover_def: "ALL l x. alg_cover l x = (SOME b. b mem l & alg_embed b x)"
  2694   by (import prob_indep alg_cover_def)
  2695 
  2696 consts
  2697   indep :: "((nat => bool) => 'a * (nat => bool)) => bool" 
  2698 
  2699 defs
  2700   indep_primdef: "indep ==
  2701 %f. EX l r.
  2702        alg_cover_set l &
  2703        (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s)))"
  2704 
  2705 lemma indep_def: "ALL f.
  2706    indep f =
  2707    (EX l r.
  2708        alg_cover_set l &
  2709        (ALL s. f s = (let c = alg_cover l s in (r c, SDROP (length c) s))))"
  2710   by (import prob_indep indep_def)
  2711 
  2712 lemma INDEP_SET_BASIC: "(All::(((nat => bool) => bool) => bool) => bool)
  2713  (%p::(nat => bool) => bool.
  2714      (op -->::bool => bool => bool)
  2715       ((measurable::((nat => bool) => bool) => bool) p)
  2716       ((op &::bool => bool => bool)
  2717         ((indep_set::((nat => bool) => bool)
  2718                      => ((nat => bool) => bool) => bool)
  2719           (EMPTY::(nat => bool) => bool) p)
  2720         ((indep_set::((nat => bool) => bool)
  2721                      => ((nat => bool) => bool) => bool)
  2722           (pred_set.UNIV::(nat => bool) => bool) p)))"
  2723   by (import prob_indep INDEP_SET_BASIC)
  2724 
  2725 lemma INDEP_SET_SYM: "ALL p q. indep_set p q = indep_set p q"
  2726   by (import prob_indep INDEP_SET_SYM)
  2727 
  2728 lemma INDEP_SET_DISJOINT_DECOMP: "(All::(((nat => bool) => bool) => bool) => bool)
  2729  (%p::(nat => bool) => bool.
  2730      (All::(((nat => bool) => bool) => bool) => bool)
  2731       (%q::(nat => bool) => bool.
  2732           (All::(((nat => bool) => bool) => bool) => bool)
  2733            (%r::(nat => bool) => bool.
  2734                (op -->::bool => bool => bool)
  2735                 ((op &::bool => bool => bool)
  2736                   ((indep_set::((nat => bool) => bool)
  2737                                => ((nat => bool) => bool) => bool)
  2738                     p r)
  2739                   ((op &::bool => bool => bool)
  2740                     ((indep_set::((nat => bool) => bool)
  2741                                  => ((nat => bool) => bool) => bool)
  2742                       q r)
  2743                     ((op =::((nat => bool) => bool)
  2744                             => ((nat => bool) => bool) => bool)
  2745                       ((pred_set.INTER::((nat => bool) => bool)
  2746   => ((nat => bool) => bool) => (nat => bool) => bool)
  2747                         p q)
  2748                       (EMPTY::(nat => bool) => bool))))
  2749                 ((indep_set::((nat => bool) => bool)
  2750                              => ((nat => bool) => bool) => bool)
  2751                   ((pred_set.UNION::((nat => bool) => bool)
  2752                                     => ((nat => bool) => bool)
  2753  => (nat => bool) => bool)
  2754                     p q)
  2755                   r))))"
  2756   by (import prob_indep INDEP_SET_DISJOINT_DECOMP)
  2757 
  2758 lemma ALG_COVER_SET_BASIC: "~ alg_cover_set [] & alg_cover_set [[]] & alg_cover_set [[True], [False]]"
  2759   by (import prob_indep ALG_COVER_SET_BASIC)
  2760 
  2761 lemma ALG_COVER_WELL_DEFINED: "(All::(bool list list => bool) => bool)
  2762  (%l::bool list list.
  2763      (All::((nat => bool) => bool) => bool)
  2764       (%x::nat => bool.
  2765           (op -->::bool => bool => bool)
  2766            ((alg_cover_set::bool list list => bool) l)
  2767            ((op &::bool => bool => bool)
  2768              ((op mem::bool list => bool list list => bool)
  2769                ((alg_cover::bool list list => (nat => bool) => bool list) l
  2770                  x)
  2771                l)
  2772              ((alg_embed::bool list => (nat => bool) => bool)
  2773                ((alg_cover::bool list list => (nat => bool) => bool list) l
  2774                  x)
  2775                x))))"
  2776   by (import prob_indep ALG_COVER_WELL_DEFINED)
  2777 
  2778 lemma ALG_COVER_UNIV: "alg_cover [[]] = K []"
  2779   by (import prob_indep ALG_COVER_UNIV)
  2780 
  2781 lemma MAP_CONS_TL_FILTER: "(All::(bool list list => bool) => bool)
  2782  (%l::bool list list.
  2783      (All::(bool => bool) => bool)
  2784       (%b::bool.
  2785           (op -->::bool => bool => bool)
  2786            ((Not::bool => bool)
  2787              ((op mem::bool list => bool list list => bool) ([]::bool list)
  2788                l))
  2789            ((op =::bool list list => bool list list => bool)
  2790              ((map::(bool list => bool list)
  2791                     => bool list list => bool list list)
  2792                ((op #::bool => bool list => bool list) b)
  2793                ((map::(bool list => bool list)
  2794                       => bool list list => bool list list)
  2795                  (tl::bool list => bool list)
  2796                  ((filter::(bool list => bool)
  2797                            => bool list list => bool list list)
  2798                    (%x::bool list.
  2799                        (op =::bool => bool => bool)
  2800                         ((hd::bool list => bool) x) b)
  2801                    l)))
  2802              ((filter::(bool list => bool)
  2803                        => bool list list => bool list list)
  2804                (%x::bool list.
  2805                    (op =::bool => bool => bool) ((hd::bool list => bool) x)
  2806                     b)
  2807                l))))"
  2808   by (import prob_indep MAP_CONS_TL_FILTER)
  2809 
  2810 lemma ALG_COVER_SET_CASES_THM: "ALL l.
  2811    alg_cover_set l =
  2812    (l = [[]] |
  2813     (EX x xa.
  2814         alg_cover_set x &
  2815         alg_cover_set xa & l = map (op # True) x @ map (op # False) xa))"
  2816   by (import prob_indep ALG_COVER_SET_CASES_THM)
  2817 
  2818 lemma ALG_COVER_SET_CASES: "(All::((bool list list => bool) => bool) => bool)
  2819  (%P::bool list list => bool.
  2820      (op -->::bool => bool => bool)
  2821       ((op &::bool => bool => bool)
  2822         (P ((op #::bool list => bool list list => bool list list)
  2823              ([]::bool list) ([]::bool list list)))
  2824         ((All::(bool list list => bool) => bool)
  2825           (%l1::bool list list.
  2826               (All::(bool list list => bool) => bool)
  2827                (%l2::bool list list.
  2828                    (op -->::bool => bool => bool)
  2829                     ((op &::bool => bool => bool)
  2830                       ((alg_cover_set::bool list list => bool) l1)
  2831                       ((op &::bool => bool => bool)
  2832                         ((alg_cover_set::bool list list => bool) l2)
  2833                         ((alg_cover_set::bool list list => bool)
  2834                           ((op @::bool list list
  2835                                   => bool list list => bool list list)
  2836                             ((map::(bool list => bool list)
  2837                                    => bool list list => bool list list)
  2838                               ((op #::bool => bool list => bool list)
  2839                                 (True::bool))
  2840                               l1)
  2841                             ((map::(bool list => bool list)
  2842                                    => bool list list => bool list list)
  2843                               ((op #::bool => bool list => bool list)
  2844                                 (False::bool))
  2845                               l2)))))
  2846                     (P ((op @::bool list list
  2847                                => bool list list => bool list list)
  2848                          ((map::(bool list => bool list)
  2849                                 => bool list list => bool list list)
  2850                            ((op #::bool => bool list => bool list)
  2851                              (True::bool))
  2852                            l1)
  2853                          ((map::(bool list => bool list)
  2854                                 => bool list list => bool list list)
  2855                            ((op #::bool => bool list => bool list)
  2856                              (False::bool))
  2857                            l2)))))))
  2858       ((All::(bool list list => bool) => bool)
  2859         (%l::bool list list.
  2860             (op -->::bool => bool => bool)
  2861              ((alg_cover_set::bool list list => bool) l) (P l))))"
  2862   by (import prob_indep ALG_COVER_SET_CASES)
  2863 
  2864 lemma ALG_COVER_SET_INDUCTION: "(All::((bool list list => bool) => bool) => bool)
  2865  (%P::bool list list => bool.
  2866      (op -->::bool => bool => bool)
  2867       ((op &::bool => bool => bool)
  2868         (P ((op #::bool list => bool list list => bool list list)
  2869              ([]::bool list) ([]::bool list list)))
  2870         ((All::(bool list list => bool) => bool)
  2871           (%l1::bool list list.
  2872               (All::(bool list list => bool) => bool)
  2873                (%l2::bool list list.
  2874                    (op -->::bool => bool => bool)
  2875                     ((op &::bool => bool => bool)
  2876                       ((alg_cover_set::bool list list => bool) l1)
  2877                       ((op &::bool => bool => bool)
  2878                         ((alg_cover_set::bool list list => bool) l2)
  2879                         ((op &::bool => bool => bool) (P l1)
  2880                           ((op &::bool => bool => bool) (P l2)
  2881                             ((alg_cover_set::bool list list => bool)
  2882                               ((op @::bool list list
  2883 => bool list list => bool list list)
  2884                                 ((map::(bool list => bool list)
  2885  => bool list list => bool list list)
  2886                                   ((op #::bool => bool list => bool list)
  2887                                     (True::bool))
  2888                                   l1)
  2889                                 ((map::(bool list => bool list)
  2890  => bool list list => bool list list)
  2891                                   ((op #::bool => bool list => bool list)
  2892                                     (False::bool))
  2893                                   l2)))))))
  2894                     (P ((op @::bool list list
  2895                                => bool list list => bool list list)
  2896                          ((map::(bool list => bool list)
  2897                                 => bool list list => bool list list)
  2898                            ((op #::bool => bool list => bool list)
  2899                              (True::bool))
  2900                            l1)
  2901                          ((map::(bool list => bool list)
  2902                                 => bool list list => bool list list)
  2903                            ((op #::bool => bool list => bool list)
  2904                              (False::bool))
  2905                            l2)))))))
  2906       ((All::(bool list list => bool) => bool)
  2907         (%l::bool list list.
  2908             (op -->::bool => bool => bool)
  2909              ((alg_cover_set::bool list list => bool) l) (P l))))"
  2910   by (import prob_indep ALG_COVER_SET_INDUCTION)
  2911 
  2912 lemma ALG_COVER_EXISTS_UNIQUE: "(All::(bool list list => bool) => bool)
  2913  (%l::bool list list.
  2914      (op -->::bool => bool => bool)
  2915       ((alg_cover_set::bool list list => bool) l)
  2916       ((All::((nat => bool) => bool) => bool)
  2917         (%s::nat => bool.
  2918             (Ex1::(bool list => bool) => bool)
  2919              (%x::bool list.
  2920                  (op &::bool => bool => bool)
  2921                   ((op mem::bool list => bool list list => bool) x l)
  2922                   ((alg_embed::bool list => (nat => bool) => bool) x s)))))"
  2923   by (import prob_indep ALG_COVER_EXISTS_UNIQUE)
  2924 
  2925 lemma ALG_COVER_UNIQUE: "(All::(bool list list => bool) => bool)
  2926  (%l::bool list list.
  2927      (All::(bool list => bool) => bool)
  2928       (%x::bool list.
  2929           (All::((nat => bool) => bool) => bool)
  2930            (%s::nat => bool.
  2931                (op -->::bool => bool => bool)
  2932                 ((op &::bool => bool => bool)
  2933                   ((alg_cover_set::bool list list => bool) l)
  2934                   ((op &::bool => bool => bool)
  2935                     ((op mem::bool list => bool list list => bool) x l)
  2936                     ((alg_embed::bool list => (nat => bool) => bool) x s)))
  2937                 ((op =::bool list => bool list => bool)
  2938                   ((alg_cover::bool list list => (nat => bool) => bool list)
  2939                     l s)
  2940                   x))))"
  2941   by (import prob_indep ALG_COVER_UNIQUE)
  2942 
  2943 lemma ALG_COVER_STEP: "(All::(bool list list => bool) => bool)
  2944  (%l1::bool list list.
  2945      (All::(bool list list => bool) => bool)
  2946       (%l2::bool list list.
  2947           (All::(bool => bool) => bool)
  2948            (%h::bool.
  2949                (All::((nat => bool) => bool) => bool)
  2950                 (%t::nat => bool.
  2951                     (op -->::bool => bool => bool)
  2952                      ((op &::bool => bool => bool)
  2953                        ((alg_cover_set::bool list list => bool) l1)
  2954                        ((alg_cover_set::bool list list => bool) l2))
  2955                      ((op =::bool list => bool list => bool)
  2956                        ((alg_cover::bool list list
  2957                                     => (nat => bool) => bool list)
  2958                          ((op @::bool list list
  2959                                  => bool list list => bool list list)
  2960                            ((map::(bool list => bool list)
  2961                                   => bool list list => bool list list)
  2962                              ((op #::bool => bool list => bool list)
  2963                                (True::bool))
  2964                              l1)
  2965                            ((map::(bool list => bool list)
  2966                                   => bool list list => bool list list)
  2967                              ((op #::bool => bool list => bool list)
  2968                                (False::bool))
  2969                              l2))
  2970                          ((SCONS::bool => (nat => bool) => nat => bool) h
  2971                            t))
  2972                        ((If::bool => bool list => bool list => bool list) h
  2973                          ((op #::bool => bool list => bool list)
  2974                            (True::bool)
  2975                            ((alg_cover::bool list list
  2976   => (nat => bool) => bool list)
  2977                              l1 t))
  2978                          ((op #::bool => bool list => bool list)
  2979                            (False::bool)
  2980                            ((alg_cover::bool list list
  2981   => (nat => bool) => bool list)
  2982                              l2 t))))))))"
  2983   by (import prob_indep ALG_COVER_STEP)
  2984 
  2985 lemma ALG_COVER_HEAD: "(All::(bool list list => bool) => bool)
  2986  (%l::bool list list.
  2987      (op -->::bool => bool => bool)
  2988       ((alg_cover_set::bool list list => bool) l)
  2989       ((All::((bool list => bool) => bool) => bool)
  2990         (%f::bool list => bool.
  2991             (op =::((nat => bool) => bool)
  2992                    => ((nat => bool) => bool) => bool)
  2993              ((op o::(bool list => bool)
  2994                      => ((nat => bool) => bool list)
  2995                         => (nat => bool) => bool)
  2996                f ((alg_cover::bool list list => (nat => bool) => bool list)
  2997                    l))
  2998              ((algebra_embed::bool list list => (nat => bool) => bool)
  2999                ((filter::(bool list => bool)
  3000                          => bool list list => bool list list)
  3001                  f l)))))"
  3002   by (import prob_indep ALG_COVER_HEAD)
  3003 
  3004 lemma ALG_COVER_TAIL_STEP: "(All::(bool list list => bool) => bool)
  3005  (%l1::bool list list.
  3006      (All::(bool list list => bool) => bool)
  3007       (%l2::bool list list.
  3008           (All::(((nat => bool) => bool) => bool) => bool)
  3009            (%q::(nat => bool) => bool.
  3010                (op -->::bool => bool => bool)
  3011                 ((op &::bool => bool => bool)
  3012                   ((alg_cover_set::bool list list => bool) l1)
  3013                   ((alg_cover_set::bool list list => bool) l2))
  3014                 ((op =::((nat => bool) => bool)
  3015                         => ((nat => bool) => bool) => bool)
  3016                   ((op o::((nat => bool) => bool)
  3017                           => ((nat => bool) => nat => bool)
  3018                              => (nat => bool) => bool)
  3019                     q (%x::nat => bool.
  3020                           (SDROP::nat => (nat => bool) => nat => bool)
  3021                            ((size::bool list => nat)
  3022                              ((alg_cover::bool list list
  3023     => (nat => bool) => bool list)
  3024                                ((op @::bool list list
  3025  => bool list list => bool list list)
  3026                                  ((map::(bool list => bool list)
  3027   => bool list list => bool list list)
  3028                                    ((op #::bool => bool list => bool list)
  3029                                      (True::bool))
  3030                                    l1)
  3031                                  ((map::(bool list => bool list)
  3032   => bool list list => bool list list)
  3033                                    ((op #::bool => bool list => bool list)
  3034                                      (False::bool))
  3035                                    l2))
  3036                                x))
  3037                            x))
  3038                   ((pred_set.UNION::((nat => bool) => bool)
  3039                                     => ((nat => bool) => bool)
  3040  => (nat => bool) => bool)
  3041                     ((pred_set.INTER::((nat => bool) => bool)
  3042 => ((nat => bool) => bool) => (nat => bool) => bool)
  3043                       (%x::nat => bool.
  3044                           (op =::bool => bool => bool)
  3045                            ((SHD::(nat => bool) => bool) x) (True::bool))
  3046                       ((op o::((nat => bool) => bool)
  3047                               => ((nat => bool) => nat => bool)
  3048                                  => (nat => bool) => bool)
  3049                         q ((op o::((nat => bool) => nat => bool)
  3050                                   => ((nat => bool) => nat => bool)
  3051                                      => (nat => bool) => nat => bool)
  3052                             (%x::nat => bool.
  3053                                 (SDROP::nat => (nat => bool) => nat => bool)
  3054                                  ((size::bool list => nat)
  3055                                    ((alg_cover::bool list list
  3056           => (nat => bool) => bool list)
  3057                                      l1 x))
  3058                                  x)
  3059                             (STL::(nat => bool) => nat => bool))))
  3060                     ((pred_set.INTER::((nat => bool) => bool)
  3061 => ((nat => bool) => bool) => (nat => bool) => bool)
  3062                       (%x::nat => bool.
  3063                           (op =::bool => bool => bool)
  3064                            ((SHD::(nat => bool) => bool) x) (False::bool))
  3065                       ((op o::((nat => bool) => bool)
  3066                               => ((nat => bool) => nat => bool)
  3067                                  => (nat => bool) => bool)
  3068                         q ((op o::((nat => bool) => nat => bool)
  3069                                   => ((nat => bool) => nat => bool)
  3070                                      => (nat => bool) => nat => bool)
  3071                             (%x::nat => bool.
  3072                                 (SDROP::nat => (nat => bool) => nat => bool)
  3073                                  ((size::bool list => nat)
  3074                                    ((alg_cover::bool list list
  3075           => (nat => bool) => bool list)
  3076                                      l2 x))
  3077                                  x)
  3078                             (STL::(nat => bool) => nat => bool)))))))))"
  3079   by (import prob_indep ALG_COVER_TAIL_STEP)
  3080 
  3081 lemma ALG_COVER_TAIL_MEASURABLE: "(All::(bool list list => bool) => bool)
  3082  (%l::bool list list.
  3083      (op -->::bool => bool => bool)
  3084       ((alg_cover_set::bool list list => bool) l)
  3085       ((All::(((nat => bool) => bool) => bool) => bool)
  3086         (%q::(nat => bool) => bool.
  3087             (op =::bool => bool => bool)
  3088              ((measurable::((nat => bool) => bool) => bool)
  3089                ((op o::((nat => bool) => bool)
  3090                        => ((nat => bool) => nat => bool)
  3091                           => (nat => bool) => bool)
  3092                  q (%x::nat => bool.
  3093                        (SDROP::nat => (nat => bool) => nat => bool)
  3094                         ((size::bool list => nat)
  3095                           ((alg_cover::bool list list
  3096  => (nat => bool) => bool list)
  3097                             l x))
  3098                         x)))
  3099              ((measurable::((nat => bool) => bool) => bool) q))))"
  3100   by (import prob_indep ALG_COVER_TAIL_MEASURABLE)
  3101 
  3102 lemma ALG_COVER_TAIL_PROB: "(All::(bool list list => bool) => bool)
  3103  (%l::bool list list.
  3104      (op -->::bool => bool => bool)
  3105       ((alg_cover_set::bool list list => bool) l)
  3106       ((All::(((nat => bool) => bool) => bool) => bool)
  3107         (%q::(nat => bool) => bool.
  3108             (op -->::bool => bool => bool)
  3109              ((measurable::((nat => bool) => bool) => bool) q)
  3110              ((op =::real => real => bool)
  3111                ((prob::((nat => bool) => bool) => real)
  3112                  ((op o::((nat => bool) => bool)
  3113                          => ((nat => bool) => nat => bool)
  3114                             => (nat => bool) => bool)
  3115                    q (%x::nat => bool.
  3116                          (SDROP::nat => (nat => bool) => nat => bool)
  3117                           ((size::bool list => nat)
  3118                             ((alg_cover::bool list list
  3119    => (nat => bool) => bool list)
  3120                               l x))
  3121                           x)))
  3122                ((prob::((nat => bool) => bool) => real) q)))))"
  3123   by (import prob_indep ALG_COVER_TAIL_PROB)
  3124 
  3125 lemma INDEP_INDEP_SET_LEMMA: "(All::(bool list list => bool) => bool)
  3126  (%l::bool list list.
  3127      (op -->::bool => bool => bool)
  3128       ((alg_cover_set::bool list list => bool) l)
  3129       ((All::(((nat => bool) => bool) => bool) => bool)
  3130         (%q::(nat => bool) => bool.
  3131             (op -->::bool => bool => bool)
  3132              ((measurable::((nat => bool) => bool) => bool) q)
  3133              ((All::(bool list => bool) => bool)
  3134                (%x::bool list.
  3135                    (op -->::bool => bool => bool)
  3136                     ((op mem::bool list => bool list list => bool) x l)
  3137                     ((op =::real => real => bool)
  3138                       ((prob::((nat => bool) => bool) => real)
  3139                         ((pred_set.INTER::((nat => bool) => bool)
  3140     => ((nat => bool) => bool) => (nat => bool) => bool)
  3141                           ((alg_embed::bool list => (nat => bool) => bool)
  3142                             x)
  3143                           ((op o::((nat => bool) => bool)
  3144                                   => ((nat => bool) => nat => bool)
  3145                                      => (nat => bool) => bool)
  3146                             q (%x::nat => bool.
  3147                                   (SDROP::nat
  3148     => (nat => bool) => nat => bool)
  3149                                    ((size::bool list => nat)
  3150                                      ((alg_cover::bool list list
  3151             => (nat => bool) => bool list)
  3152  l x))
  3153                                    x))))
  3154                       ((op *::real => real => real)
  3155                         ((op ^::real => nat => real)
  3156                           ((op /::real => real => real) (1::real)
  3157                             ((number_of::bin => real)
  3158                               ((op BIT::bin => bool => bin)
  3159                                 ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3160                                   (True::bool))
  3161                                 (False::bool))))
  3162                           ((size::bool list => nat) x))
  3163                         ((prob::((nat => bool) => bool) => real) q))))))))"
  3164   by (import prob_indep INDEP_INDEP_SET_LEMMA)
  3165 
  3166 lemma INDEP_SET_LIST: "(All::(((nat => bool) => bool) => bool) => bool)
  3167  (%q::(nat => bool) => bool.
  3168      (All::(bool list list => bool) => bool)
  3169       (%l::bool list list.
  3170           (op -->::bool => bool => bool)
  3171            ((op &::bool => bool => bool)
  3172              ((alg_sorted::bool list list => bool) l)
  3173              ((op &::bool => bool => bool)
  3174                ((alg_prefixfree::bool list list => bool) l)
  3175                ((op &::bool => bool => bool)
  3176                  ((measurable::((nat => bool) => bool) => bool) q)
  3177                  ((All::(bool list => bool) => bool)
  3178                    (%x::bool list.
  3179                        (op -->::bool => bool => bool)
  3180                         ((op mem::bool list => bool list list => bool) x l)
  3181                         ((indep_set::((nat => bool) => bool)
  3182                                      => ((nat => bool) => bool) => bool)
  3183                           ((alg_embed::bool list => (nat => bool) => bool)
  3184                             x)
  3185                           q))))))
  3186            ((indep_set::((nat => bool) => bool)
  3187                         => ((nat => bool) => bool) => bool)
  3188              ((algebra_embed::bool list list => (nat => bool) => bool) l)
  3189              q)))"
  3190   by (import prob_indep INDEP_SET_LIST)
  3191 
  3192 lemma INDEP_INDEP_SET: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3193  (%f::(nat => bool) => 'a * (nat => bool).
  3194      (All::(('a => bool) => bool) => bool)
  3195       (%p::'a => bool.
  3196           (All::(((nat => bool) => bool) => bool) => bool)
  3197            (%q::(nat => bool) => bool.
  3198                (op -->::bool => bool => bool)
  3199                 ((op &::bool => bool => bool)
  3200                   ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  3201                   ((measurable::((nat => bool) => bool) => bool) q))
  3202                 ((indep_set::((nat => bool) => bool)
  3203                              => ((nat => bool) => bool) => bool)
  3204                   ((op o::('a => bool)
  3205                           => ((nat => bool) => 'a) => (nat => bool) => bool)
  3206                     p ((op o::('a * (nat => bool) => 'a)
  3207                               => ((nat => bool) => 'a * (nat => bool))
  3208                                  => (nat => bool) => 'a)
  3209                         (fst::'a * (nat => bool) => 'a) f))
  3210                   ((op o::((nat => bool) => bool)
  3211                           => ((nat => bool) => nat => bool)
  3212                              => (nat => bool) => bool)
  3213                     q ((op o::('a * (nat => bool) => nat => bool)
  3214                               => ((nat => bool) => 'a * (nat => bool))
  3215                                  => (nat => bool) => nat => bool)
  3216                         (snd::'a * (nat => bool) => nat => bool) f))))))"
  3217   by (import prob_indep INDEP_INDEP_SET)
  3218 
  3219 lemma INDEP_UNIT: "ALL x. indep (UNIT x)"
  3220   by (import prob_indep INDEP_UNIT)
  3221 
  3222 lemma INDEP_SDEST: "indep SDEST"
  3223   by (import prob_indep INDEP_SDEST)
  3224 
  3225 lemma BIND_STEP: "ALL f. BIND SDEST (%k. f o SCONS k) = f"
  3226   by (import prob_indep BIND_STEP)
  3227 
  3228 lemma INDEP_BIND_SDEST: "(All::((bool => (nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3229  (%f::bool => (nat => bool) => 'a * (nat => bool).
  3230      (op -->::bool => bool => bool)
  3231       ((All::(bool => bool) => bool)
  3232         (%x::bool.
  3233             (indep::((nat => bool) => 'a * (nat => bool)) => bool) (f x)))
  3234       ((indep::((nat => bool) => 'a * (nat => bool)) => bool)
  3235         ((BIND::((nat => bool) => bool * (nat => bool))
  3236                 => (bool => (nat => bool) => 'a * (nat => bool))
  3237                    => (nat => bool) => 'a * (nat => bool))
  3238           (SDEST::(nat => bool) => bool * (nat => bool)) f)))"
  3239   by (import prob_indep INDEP_BIND_SDEST)
  3240 
  3241 lemma INDEP_BIND: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3242  (%f::(nat => bool) => 'a * (nat => bool).
  3243      (All::(('a => (nat => bool) => 'b * (nat => bool)) => bool) => bool)
  3244       (%g::'a => (nat => bool) => 'b * (nat => bool).
  3245           (op -->::bool => bool => bool)
  3246            ((op &::bool => bool => bool)
  3247              ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  3248              ((All::('a => bool) => bool)
  3249                (%x::'a.
  3250                    (indep::((nat => bool) => 'b * (nat => bool)) => bool)
  3251                     (g x))))
  3252            ((indep::((nat => bool) => 'b * (nat => bool)) => bool)
  3253              ((BIND::((nat => bool) => 'a * (nat => bool))
  3254                      => ('a => (nat => bool) => 'b * (nat => bool))
  3255                         => (nat => bool) => 'b * (nat => bool))
  3256                f g))))"
  3257   by (import prob_indep INDEP_BIND)
  3258 
  3259 lemma INDEP_PROB: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3260  (%f::(nat => bool) => 'a * (nat => bool).
  3261      (All::(('a => bool) => bool) => bool)
  3262       (%p::'a => bool.
  3263           (All::(((nat => bool) => bool) => bool) => bool)
  3264            (%q::(nat => bool) => bool.
  3265                (op -->::bool => bool => bool)
  3266                 ((op &::bool => bool => bool)
  3267                   ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  3268                   ((measurable::((nat => bool) => bool) => bool) q))
  3269                 ((op =::real => real => bool)
  3270                   ((prob::((nat => bool) => bool) => real)
  3271                     ((pred_set.INTER::((nat => bool) => bool)
  3272 => ((nat => bool) => bool) => (nat => bool) => bool)
  3273                       ((op o::('a => bool)
  3274                               => ((nat => bool) => 'a)
  3275                                  => (nat => bool) => bool)
  3276                         p ((op o::('a * (nat => bool) => 'a)
  3277                                   => ((nat => bool) => 'a * (nat => bool))
  3278                                      => (nat => bool) => 'a)
  3279                             (fst::'a * (nat => bool) => 'a) f))
  3280                       ((op o::((nat => bool) => bool)
  3281                               => ((nat => bool) => nat => bool)
  3282                                  => (nat => bool) => bool)
  3283                         q ((op o::('a * (nat => bool) => nat => bool)
  3284                                   => ((nat => bool) => 'a * (nat => bool))
  3285                                      => (nat => bool) => nat => bool)
  3286                             (snd::'a * (nat => bool) => nat => bool) f))))
  3287                   ((op *::real => real => real)
  3288                     ((prob::((nat => bool) => bool) => real)
  3289                       ((op o::('a => bool)
  3290                               => ((nat => bool) => 'a)
  3291                                  => (nat => bool) => bool)
  3292                         p ((op o::('a * (nat => bool) => 'a)
  3293                                   => ((nat => bool) => 'a * (nat => bool))
  3294                                      => (nat => bool) => 'a)
  3295                             (fst::'a * (nat => bool) => 'a) f)))
  3296                     ((prob::((nat => bool) => bool) => real) q))))))"
  3297   by (import prob_indep INDEP_PROB)
  3298 
  3299 lemma INDEP_MEASURABLE1: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3300  (%f::(nat => bool) => 'a * (nat => bool).
  3301      (All::(('a => bool) => bool) => bool)
  3302       (%p::'a => bool.
  3303           (op -->::bool => bool => bool)
  3304            ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  3305            ((measurable::((nat => bool) => bool) => bool)
  3306              ((op o::('a => bool)
  3307                      => ((nat => bool) => 'a) => (nat => bool) => bool)
  3308                p ((op o::('a * (nat => bool) => 'a)
  3309                          => ((nat => bool) => 'a * (nat => bool))
  3310                             => (nat => bool) => 'a)
  3311                    (fst::'a * (nat => bool) => 'a) f)))))"
  3312   by (import prob_indep INDEP_MEASURABLE1)
  3313 
  3314 lemma INDEP_MEASURABLE2: "(All::(((nat => bool) => 'a * (nat => bool)) => bool) => bool)
  3315  (%f::(nat => bool) => 'a * (nat => bool).
  3316      (All::(((nat => bool) => bool) => bool) => bool)
  3317       (%q::(nat => bool) => bool.
  3318           (op -->::bool => bool => bool)
  3319            ((op &::bool => bool => bool)
  3320              ((indep::((nat => bool) => 'a * (nat => bool)) => bool) f)
  3321              ((measurable::((nat => bool) => bool) => bool) q))
  3322            ((measurable::((nat => bool) => bool) => bool)
  3323              ((op o::((nat => bool) => bool)
  3324                      => ((nat => bool) => nat => bool)
  3325                         => (nat => bool) => bool)
  3326                q ((op o::('a * (nat => bool) => nat => bool)
  3327                          => ((nat => bool) => 'a * (nat => bool))
  3328                             => (nat => bool) => nat => bool)
  3329                    (snd::'a * (nat => bool) => nat => bool) f)))))"
  3330   by (import prob_indep INDEP_MEASURABLE2)
  3331 
  3332 lemma PROB_INDEP_BOUND: "(All::(((nat => bool) => nat * (nat => bool)) => bool) => bool)
  3333  (%f::(nat => bool) => nat * (nat => bool).
  3334      (All::(nat => bool) => bool)
  3335       (%n::nat.
  3336           (op -->::bool => bool => bool)
  3337            ((indep::((nat => bool) => nat * (nat => bool)) => bool) f)
  3338            ((op =::real => real => bool)
  3339              ((prob::((nat => bool) => bool) => real)
  3340                (%s::nat => bool.
  3341                    (op <::nat => nat => bool)
  3342                     ((fst::nat * (nat => bool) => nat) (f s))
  3343                     ((Suc::nat => nat) n)))
  3344              ((op +::real => real => real)
  3345                ((prob::((nat => bool) => bool) => real)
  3346                  (%s::nat => bool.
  3347                      (op <::nat => nat => bool)
  3348                       ((fst::nat * (nat => bool) => nat) (f s)) n))
  3349                ((prob::((nat => bool) => bool) => real)
  3350                  (%s::nat => bool.
  3351                      (op =::nat => nat => bool)
  3352                       ((fst::nat * (nat => bool) => nat) (f s)) n))))))"
  3353   by (import prob_indep PROB_INDEP_BOUND)
  3354 
  3355 ;end_setup
  3356 
  3357 ;setup_theory prob_uniform
  3358 
  3359 consts
  3360   unif_bound :: "nat => nat" 
  3361 
  3362 defs
  3363   unif_bound_primdef: "unif_bound ==
  3364 WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
  3365  (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
  3366 
  3367 lemma unif_bound_primitive_def: "unif_bound =
  3368 WFREC (SOME R. WF R & (ALL v. R (Suc v div 2) (Suc v)))
  3369  (%unif_bound. nat_case 0 (%v1. Suc (unif_bound (Suc v1 div 2))))"
  3370   by (import prob_uniform unif_bound_primitive_def)
  3371 
  3372 lemma unif_bound_def: "unif_bound 0 = 0 & unif_bound (Suc v) = Suc (unif_bound (Suc v div 2))"
  3373   by (import prob_uniform unif_bound_def)
  3374 
  3375 lemma unif_bound_ind: "(All::((nat => bool) => bool) => bool)
  3376  (%P::nat => bool.
  3377      (op -->::bool => bool => bool)
  3378       ((op &::bool => bool => bool) (P (0::nat))
  3379         ((All::(nat => bool) => bool)
  3380           (%v::nat.
  3381               (op -->::bool => bool => bool)
  3382                (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
  3383                     ((number_of::bin => nat)
  3384                       ((op BIT::bin => bool => bin)
  3385                         ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3386                           (True::bool))
  3387                         (False::bool)))))
  3388                (P ((Suc::nat => nat) v)))))
  3389       ((All::(nat => bool) => bool) P))"
  3390   by (import prob_uniform unif_bound_ind)
  3391 
  3392 constdefs
  3393   unif_tupled :: "nat * (nat => bool) => nat * (nat => bool)" 
  3394   "unif_tupled ==
  3395 WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
  3396  (%unif_tupled (v, v1).
  3397      case v of 0 => (0, v1)
  3398      | Suc v3 =>
  3399          let (m, s') = unif_tupled (Suc v3 div 2, v1)
  3400          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  3401 
  3402 lemma unif_tupled_primitive_def: "unif_tupled =
  3403 WFREC (SOME R. WF R & (ALL s v2. R (Suc v2 div 2, s) (Suc v2, s)))
  3404  (%unif_tupled (v, v1).
  3405      case v of 0 => (0, v1)
  3406      | Suc v3 =>
  3407          let (m, s') = unif_tupled (Suc v3 div 2, v1)
  3408          in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  3409   by (import prob_uniform unif_tupled_primitive_def)
  3410 
  3411 consts
  3412   unif :: "nat => (nat => bool) => nat * (nat => bool)" 
  3413 
  3414 defs
  3415   unif_primdef: "unif == %x x1. unif_tupled (x, x1)"
  3416 
  3417 lemma unif_curried_def: "ALL x x1. unif x x1 = unif_tupled (x, x1)"
  3418   by (import prob_uniform unif_curried_def)
  3419 
  3420 lemma unif_def: "unif 0 s = (0, s) &
  3421 unif (Suc v2) s =
  3422 (let (m, s') = unif (Suc v2 div 2) s
  3423  in (if SHD s' then 2 * m + 1 else 2 * m, STL s'))"
  3424   by (import prob_uniform unif_def)
  3425 
  3426 lemma unif_ind: "(All::((nat => (nat => bool) => bool) => bool) => bool)
  3427  (%P::nat => (nat => bool) => bool.
  3428      (op -->::bool => bool => bool)
  3429       ((op &::bool => bool => bool)
  3430         ((All::((nat => bool) => bool) => bool) (P (0::nat)))
  3431         ((All::(nat => bool) => bool)
  3432           (%v2::nat.
  3433               (All::((nat => bool) => bool) => bool)
  3434                (%s::nat => bool.
  3435                    (op -->::bool => bool => bool)
  3436                     (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
  3437                          ((number_of::bin => nat)
  3438                            ((op BIT::bin => bool => bin)
  3439                              ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3440                                (True::bool))
  3441                              (False::bool))))
  3442                       s)
  3443                     (P ((Suc::nat => nat) v2) s)))))
  3444       ((All::(nat => bool) => bool)
  3445         (%v::nat. (All::((nat => bool) => bool) => bool) (P v))))"
  3446   by (import prob_uniform unif_ind)
  3447 
  3448 constdefs
  3449   uniform_tupled :: "nat * nat * (nat => bool) => nat * (nat => bool)" 
  3450   "(op ==::(nat * nat * (nat => bool) => nat * (nat => bool))
  3451         => (nat * nat * (nat => bool) => nat * (nat => bool)) => prop)
  3452  (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  3453  ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3454           => ((nat * nat * (nat => bool) => nat * (nat => bool))
  3455               => nat * nat * (nat => bool) => nat * (nat => bool))
  3456              => nat * nat * (nat => bool) => nat * (nat => bool))
  3457    ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3458            => bool)
  3459           => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3460      (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  3461          (op &::bool => bool => bool)
  3462           ((WF::(nat * nat * (nat => bool)
  3463                  => nat * nat * (nat => bool) => bool)
  3464                 => bool)
  3465             R)
  3466           ((All::(nat => bool) => bool)
  3467             (%t::nat.
  3468                 (All::((nat => bool) => bool) => bool)
  3469                  (%s::nat => bool.
  3470                      (All::(nat => bool) => bool)
  3471                       (%n::nat.
  3472                           (All::(nat => bool) => bool)
  3473                            (%res::nat.
  3474                                (All::((nat => bool) => bool) => bool)
  3475                                 (%s'::nat => bool.
  3476                                     (op -->::bool => bool => bool)
  3477                                      ((op &::bool => bool => bool)
  3478  ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  3479    ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
  3480    ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
  3481  ((Not::bool => bool)
  3482    ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
  3483                                      (R
  3484  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
  3485    ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3486      ((Suc::nat => nat) n) s'))
  3487  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
  3488    ((Suc::nat => nat) t)
  3489    ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3490      ((Suc::nat => nat) n) s)))))))))))
  3491    (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
  3492        (split::(nat => nat * (nat => bool) => nat * (nat => bool))
  3493                => nat * nat * (nat => bool) => nat * (nat => bool))
  3494         (%(v::nat) v1::nat * (nat => bool).
  3495             (nat_case::nat * (nat => bool)
  3496                        => (nat => nat * (nat => bool))
  3497                           => nat => nat * (nat => bool))
  3498              ((split::(nat => (nat => bool) => nat * (nat => bool))
  3499                       => nat * (nat => bool) => nat * (nat => bool))
  3500                (%(v3::nat) v4::nat => bool.
  3501                    (nat_case::nat * (nat => bool)
  3502                               => (nat => nat * (nat => bool))
  3503                                  => nat => nat * (nat => bool))
  3504                     (ARB::nat * (nat => bool))
  3505                     (%v5::nat.
  3506                         (Pair::nat => (nat => bool) => nat * (nat => bool))
  3507                          (0::nat) v4)
  3508                     v3)
  3509                v1)
  3510              (%v2::nat.
  3511                  (split::(nat => (nat => bool) => nat * (nat => bool))
  3512                          => nat * (nat => bool) => nat * (nat => bool))
  3513                   (%(v7::nat) v8::nat => bool.
  3514                       (nat_case::nat * (nat => bool)
  3515                                  => (nat => nat * (nat => bool))
  3516                                     => nat => nat * (nat => bool))
  3517                        (ARB::nat * (nat => bool))
  3518                        (%v9::nat.
  3519                            (Let::nat * (nat => bool)
  3520                                  => (nat * (nat => bool)
  3521                                      => nat * (nat => bool))
  3522                                     => nat * (nat => bool))
  3523                             ((unif::nat
  3524                                     => (nat => bool) => nat * (nat => bool))
  3525                               v9 v8)
  3526                             ((split::(nat
  3527 => (nat => bool) => nat * (nat => bool))
  3528                                      => nat * (nat => bool)
  3529   => nat * (nat => bool))
  3530                               (%(res::nat) s'::nat => bool.
  3531                                   (If::bool
  3532  => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
  3533                                    ((op <::nat => nat => bool) res
  3534                                      ((Suc::nat => nat) v9))
  3535                                    ((Pair::nat
  3536      => (nat => bool) => nat * (nat => bool))
  3537                                      res s')
  3538                                    (uniform_tupled
  3539                                      ((Pair::nat
  3540        => nat * (nat => bool) => nat * nat * (nat => bool))
  3541  v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3542       ((Suc::nat => nat) v9) s'))))))
  3543                        v7)
  3544                   v1)
  3545              v)))"
  3546 
  3547 lemma uniform_tupled_primitive_def: "(op =::(nat * nat * (nat => bool) => nat * (nat => bool))
  3548        => (nat * nat * (nat => bool) => nat * (nat => bool)) => bool)
  3549  (uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool))
  3550  ((WFREC::(nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3551           => ((nat * nat * (nat => bool) => nat * (nat => bool))
  3552               => nat * nat * (nat => bool) => nat * (nat => bool))
  3553              => nat * nat * (nat => bool) => nat * (nat => bool))
  3554    ((Eps::((nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3555            => bool)
  3556           => nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool)
  3557      (%R::nat * nat * (nat => bool) => nat * nat * (nat => bool) => bool.
  3558          (op &::bool => bool => bool)
  3559           ((WF::(nat * nat * (nat => bool)
  3560                  => nat * nat * (nat => bool) => bool)
  3561                 => bool)
  3562             R)
  3563           ((All::(nat => bool) => bool)
  3564             (%t::nat.
  3565                 (All::((nat => bool) => bool) => bool)
  3566                  (%s::nat => bool.
  3567                      (All::(nat => bool) => bool)
  3568                       (%n::nat.
  3569                           (All::(nat => bool) => bool)
  3570                            (%res::nat.
  3571                                (All::((nat => bool) => bool) => bool)
  3572                                 (%s'::nat => bool.
  3573                                     (op -->::bool => bool => bool)
  3574                                      ((op &::bool => bool => bool)
  3575  ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  3576    ((Pair::nat => (nat => bool) => nat * (nat => bool)) res s')
  3577    ((unif::nat => (nat => bool) => nat * (nat => bool)) n s))
  3578  ((Not::bool => bool)
  3579    ((op <::nat => nat => bool) res ((Suc::nat => nat) n))))
  3580                                      (R
  3581  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool)) t
  3582    ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3583      ((Suc::nat => nat) n) s'))
  3584  ((Pair::nat => nat * (nat => bool) => nat * nat * (nat => bool))
  3585    ((Suc::nat => nat) t)
  3586    ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3587      ((Suc::nat => nat) n) s)))))))))))
  3588    (%uniform_tupled::nat * nat * (nat => bool) => nat * (nat => bool).
  3589        (split::(nat => nat * (nat => bool) => nat * (nat => bool))
  3590                => nat * nat * (nat => bool) => nat * (nat => bool))
  3591         (%(v::nat) v1::nat * (nat => bool).
  3592             (nat_case::nat * (nat => bool)
  3593                        => (nat => nat * (nat => bool))
  3594                           => nat => nat * (nat => bool))
  3595              ((split::(nat => (nat => bool) => nat * (nat => bool))
  3596                       => nat * (nat => bool) => nat * (nat => bool))
  3597                (%(v3::nat) v4::nat => bool.
  3598                    (nat_case::nat * (nat => bool)
  3599                               => (nat => nat * (nat => bool))
  3600                                  => nat => nat * (nat => bool))
  3601                     (ARB::nat * (nat => bool))
  3602                     (%v5::nat.
  3603                         (Pair::nat => (nat => bool) => nat * (nat => bool))
  3604                          (0::nat) v4)
  3605                     v3)
  3606                v1)
  3607              (%v2::nat.
  3608                  (split::(nat => (nat => bool) => nat * (nat => bool))
  3609                          => nat * (nat => bool) => nat * (nat => bool))
  3610                   (%(v7::nat) v8::nat => bool.
  3611                       (nat_case::nat * (nat => bool)
  3612                                  => (nat => nat * (nat => bool))
  3613                                     => nat => nat * (nat => bool))
  3614                        (ARB::nat * (nat => bool))
  3615                        (%v9::nat.
  3616                            (Let::nat * (nat => bool)
  3617                                  => (nat * (nat => bool)
  3618                                      => nat * (nat => bool))
  3619                                     => nat * (nat => bool))
  3620                             ((unif::nat
  3621                                     => (nat => bool) => nat * (nat => bool))
  3622                               v9 v8)
  3623                             ((split::(nat
  3624 => (nat => bool) => nat * (nat => bool))
  3625                                      => nat * (nat => bool)
  3626   => nat * (nat => bool))
  3627                               (%(res::nat) s'::nat => bool.
  3628                                   (If::bool
  3629  => nat * (nat => bool) => nat * (nat => bool) => nat * (nat => bool))
  3630                                    ((op <::nat => nat => bool) res
  3631                                      ((Suc::nat => nat) v9))
  3632                                    ((Pair::nat
  3633      => (nat => bool) => nat * (nat => bool))
  3634                                      res s')
  3635                                    (uniform_tupled
  3636                                      ((Pair::nat
  3637        => nat * (nat => bool) => nat * nat * (nat => bool))
  3638  v2 ((Pair::nat => (nat => bool) => nat * (nat => bool))
  3639       ((Suc::nat => nat) v9) s'))))))
  3640                        v7)
  3641                   v1)
  3642              v)))"
  3643   by (import prob_uniform uniform_tupled_primitive_def)
  3644 
  3645 consts
  3646   uniform :: "nat => nat => (nat => bool) => nat * (nat => bool)" 
  3647 
  3648 defs
  3649   uniform_primdef: "uniform == %x x1 x2. uniform_tupled (x, x1, x2)"
  3650 
  3651 lemma uniform_curried_def: "ALL x x1 x2. uniform x x1 x2 = uniform_tupled (x, x1, x2)"
  3652   by (import prob_uniform uniform_curried_def)
  3653 
  3654 lemma uniform_ind: "(All::((nat => nat => (nat => bool) => bool) => bool) => bool)
  3655  (%P::nat => nat => (nat => bool) => bool.
  3656      (op -->::bool => bool => bool)
  3657       ((op &::bool => bool => bool)
  3658         ((All::(nat => bool) => bool)
  3659           (%x::nat.
  3660               (All::((nat => bool) => bool) => bool)
  3661                (P ((Suc::nat => nat) x) (0::nat))))
  3662         ((op &::bool => bool => bool)
  3663           ((All::((nat => bool) => bool) => bool) (P (0::nat) (0::nat)))
  3664           ((op &::bool => bool => bool)
  3665             ((All::(nat => bool) => bool)
  3666               (%x::nat.
  3667                   (All::((nat => bool) => bool) => bool)
  3668                    (P (0::nat) ((Suc::nat => nat) x))))
  3669             ((All::(nat => bool) => bool)
  3670               (%x::nat.
  3671                   (All::(nat => bool) => bool)
  3672                    (%xa::nat.
  3673                        (All::((nat => bool) => bool) => bool)
  3674                         (%xb::nat => bool.
  3675                             (op -->::bool => bool => bool)
  3676                              ((All::(nat => bool) => bool)
  3677                                (%xc::nat.
  3678                                    (All::((nat => bool) => bool) => bool)
  3679                                     (%xd::nat => bool.
  3680   (op -->::bool => bool => bool)
  3681    ((op &::bool => bool => bool)
  3682      ((op =::nat * (nat => bool) => nat * (nat => bool) => bool)
  3683        ((Pair::nat => (nat => bool) => nat * (nat => bool)) xc xd)
  3684        ((unif::nat => (nat => bool) => nat * (nat => bool)) xa xb))
  3685      ((Not::bool => bool)
  3686        ((op <::nat => nat => bool) xc ((Suc::nat => nat) xa))))
  3687    (P x ((Suc::nat => nat) xa) xd))))
  3688                              (P ((Suc::nat => nat) x) ((Suc::nat => nat) xa)
  3689                                xb))))))))
  3690       ((All::(nat => bool) => bool)
  3691         (%x::nat.
  3692             (All::(nat => bool) => bool)
  3693              (%xa::nat. (All::((nat => bool) => bool) => bool) (P x xa)))))"
  3694   by (import prob_uniform uniform_ind)
  3695 
  3696 lemma uniform_def: "uniform 0 (Suc n) s = (0, s) &
  3697 uniform (Suc t) (Suc n) s =
  3698 (let (xa, x) = unif n s
  3699  in if xa < Suc n then (xa, x) else uniform t (Suc n) x)"
  3700   by (import prob_uniform uniform_def)
  3701 
  3702 lemma SUC_DIV_TWO_ZERO: "ALL n. (Suc n div 2 = 0) = (n = 0)"
  3703   by (import prob_uniform SUC_DIV_TWO_ZERO)
  3704 
  3705 lemma UNIF_BOUND_LOWER: "ALL n. n < 2 ^ unif_bound n"
  3706   by (import prob_uniform UNIF_BOUND_LOWER)
  3707 
  3708 lemma UNIF_BOUND_LOWER_SUC: "ALL n. Suc n <= 2 ^ unif_bound n"
  3709   by (import prob_uniform UNIF_BOUND_LOWER_SUC)
  3710 
  3711 lemma UNIF_BOUND_UPPER: "(All::(nat => bool) => bool)
  3712  (%n::nat.
  3713      (op -->::bool => bool => bool)
  3714       ((Not::bool => bool) ((op =::nat => nat => bool) n (0::nat)))
  3715       ((op <=::nat => nat => bool)
  3716         ((op ^::nat => nat => nat)
  3717           ((number_of::bin => nat)
  3718             ((op BIT::bin => bool => bin)
  3719               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
  3720               (False::bool)))
  3721           ((unif_bound::nat => nat) n))
  3722         ((op *::nat => nat => nat)
  3723           ((number_of::bin => nat)
  3724             ((op BIT::bin => bool => bin)
  3725               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
  3726               (False::bool)))
  3727           n)))"
  3728   by (import prob_uniform UNIF_BOUND_UPPER)
  3729 
  3730 lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)"
  3731   by (import prob_uniform UNIF_BOUND_UPPER_SUC)
  3732 
  3733 lemma UNIF_DEF_MONAD: "unif 0 = UNIT 0 &
  3734 (ALL n.
  3735     unif (Suc n) =
  3736     BIND (unif (Suc n div 2))
  3737      (%m. BIND SDEST (%b. UNIT (if b then 2 * m + 1 else 2 * m))))"
  3738   by (import prob_uniform UNIF_DEF_MONAD)
  3739 
  3740 lemma UNIFORM_DEF_MONAD: "(ALL x. uniform 0 (Suc x) = UNIT 0) &
  3741 (ALL x xa.
  3742     uniform (Suc x) (Suc xa) =
  3743     BIND (unif xa) (%m. if m < Suc xa then UNIT m else uniform x (Suc xa)))"
  3744   by (import prob_uniform UNIFORM_DEF_MONAD)
  3745 
  3746 lemma INDEP_UNIF: "ALL n. indep (unif n)"
  3747   by (import prob_uniform INDEP_UNIF)
  3748 
  3749 lemma INDEP_UNIFORM: "ALL t n. indep (uniform t (Suc n))"
  3750   by (import prob_uniform INDEP_UNIFORM)
  3751 
  3752 lemma PROB_UNIF: "ALL n k.
  3753    prob (%s. fst (unif n s) = k) =
  3754    (if k < 2 ^ unif_bound n then (1 / 2) ^ unif_bound n else 0)"
  3755   by (import prob_uniform PROB_UNIF)
  3756 
  3757 lemma UNIF_RANGE: "ALL n s. fst (unif n s) < 2 ^ unif_bound n"
  3758   by (import prob_uniform UNIF_RANGE)
  3759 
  3760 lemma PROB_UNIF_PAIR: "ALL n k k'.
  3761    (prob (%s. fst (unif n s) = k) = prob (%s. fst (unif n s) = k')) =
  3762    ((k < 2 ^ unif_bound n) = (k' < 2 ^ unif_bound n))"
  3763   by (import prob_uniform PROB_UNIF_PAIR)
  3764 
  3765 lemma PROB_UNIF_BOUND: "(All::(nat => bool) => bool)
  3766  (%n::nat.
  3767      (All::(nat => bool) => bool)
  3768       (%k::nat.
  3769           (op -->::bool => bool => bool)
  3770            ((op <=::nat => nat => bool) k
  3771              ((op ^::nat => nat => nat)
  3772                ((number_of::bin => nat)
  3773                  ((op BIT::bin => bool => bin)
  3774                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3775                      (True::bool))
  3776                    (False::bool)))
  3777                ((unif_bound::nat => nat) n)))
  3778            ((op =::real => real => bool)
  3779              ((prob::((nat => bool) => bool) => real)
  3780                (%s::nat => bool.
  3781                    (op <::nat => nat => bool)
  3782                     ((fst::nat * (nat => bool) => nat)
  3783                       ((unif::nat => (nat => bool) => nat * (nat => bool)) n
  3784                         s))
  3785                     k))
  3786              ((op *::real => real => real) ((real::nat => real) k)
  3787                ((op ^::real => nat => real)
  3788                  ((op /::real => real => real) (1::real)
  3789                    ((number_of::bin => real)
  3790                      ((op BIT::bin => bool => bin)
  3791                        ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3792                          (True::bool))
  3793                        (False::bool))))
  3794                  ((unif_bound::nat => nat) n))))))"
  3795   by (import prob_uniform PROB_UNIF_BOUND)
  3796 
  3797 lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)"
  3798   by (import prob_uniform PROB_UNIF_GOOD)
  3799 
  3800 lemma UNIFORM_RANGE: "ALL t n s. fst (uniform t (Suc n) s) < Suc n"
  3801   by (import prob_uniform UNIFORM_RANGE)
  3802 
  3803 lemma PROB_UNIFORM_LOWER_BOUND: "(All::(real => bool) => bool)
  3804  (%b::real.
  3805      (op -->::bool => bool => bool)
  3806       ((All::(nat => bool) => bool)
  3807         (%k::nat.
  3808             (op -->::bool => bool => bool)
  3809              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  3810              ((op <::real => real => bool)
  3811                ((prob::((nat => bool) => bool) => real)
  3812                  (%s::nat => bool.
  3813                      (op =::nat => nat => bool)
  3814                       ((fst::nat * (nat => bool) => nat)
  3815                         ((uniform::nat
  3816                                    => nat
  3817 => (nat => bool) => nat * (nat => bool))
  3818                           (t::nat) ((Suc::nat => nat) n) s))
  3819                       k))
  3820                b)))
  3821       ((All::(nat => bool) => bool)
  3822         (%m::nat.
  3823             (op -->::bool => bool => bool)
  3824              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  3825              ((op <::real => real => bool)
  3826                ((prob::((nat => bool) => bool) => real)
  3827                  (%s::nat => bool.
  3828                      (op <::nat => nat => bool)
  3829                       ((fst::nat * (nat => bool) => nat)
  3830                         ((uniform::nat
  3831                                    => nat
  3832 => (nat => bool) => nat * (nat => bool))
  3833                           t ((Suc::nat => nat) n) s))
  3834                       ((Suc::nat => nat) m)))
  3835                ((op *::real => real => real)
  3836                  ((real::nat => real) ((Suc::nat => nat) m)) b)))))"
  3837   by (import prob_uniform PROB_UNIFORM_LOWER_BOUND)
  3838 
  3839 lemma PROB_UNIFORM_UPPER_BOUND: "(All::(real => bool) => bool)
  3840  (%b::real.
  3841      (op -->::bool => bool => bool)
  3842       ((All::(nat => bool) => bool)
  3843         (%k::nat.
  3844             (op -->::bool => bool => bool)
  3845              ((op <::nat => nat => bool) k ((Suc::nat => nat) (n::nat)))
  3846              ((op <::real => real => bool) b
  3847                ((prob::((nat => bool) => bool) => real)
  3848                  (%s::nat => bool.
  3849                      (op =::nat => nat => bool)
  3850                       ((fst::nat * (nat => bool) => nat)
  3851                         ((uniform::nat
  3852                                    => nat
  3853 => (nat => bool) => nat * (nat => bool))
  3854                           (t::nat) ((Suc::nat => nat) n) s))
  3855                       k)))))
  3856       ((All::(nat => bool) => bool)
  3857         (%m::nat.
  3858             (op -->::bool => bool => bool)
  3859              ((op <::nat => nat => bool) m ((Suc::nat => nat) n))
  3860              ((op <::real => real => bool)
  3861                ((op *::real => real => real)
  3862                  ((real::nat => real) ((Suc::nat => nat) m)) b)
  3863                ((prob::((nat => bool) => bool) => real)
  3864                  (%s::nat => bool.
  3865                      (op <::nat => nat => bool)
  3866                       ((fst::nat * (nat => bool) => nat)
  3867                         ((uniform::nat
  3868                                    => nat
  3869 => (nat => bool) => nat * (nat => bool))
  3870                           t ((Suc::nat => nat) n) s))
  3871                       ((Suc::nat => nat) m)))))))"
  3872   by (import prob_uniform PROB_UNIFORM_UPPER_BOUND)
  3873 
  3874 lemma PROB_UNIFORM_PAIR_SUC: "(All::(nat => bool) => bool)
  3875  (%t::nat.
  3876      (All::(nat => bool) => bool)
  3877       (%n::nat.
  3878           (All::(nat => bool) => bool)
  3879            (%k::nat.
  3880                (All::(nat => bool) => bool)
  3881                 (%k'::nat.
  3882                     (op -->::bool => bool => bool)
  3883                      ((op &::bool => bool => bool)
  3884                        ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
  3885                        ((op <::nat => nat => bool) k'
  3886                          ((Suc::nat => nat) n)))
  3887                      ((op <=::real => real => bool)
  3888                        ((abs::real => real)
  3889                          ((op -::real => real => real)
  3890                            ((prob::((nat => bool) => bool) => real)
  3891                              (%s::nat => bool.
  3892                                  (op =::nat => nat => bool)
  3893                                   ((fst::nat * (nat => bool) => nat)
  3894                                     ((uniform::nat
  3895          => nat => (nat => bool) => nat * (nat => bool))
  3896 t ((Suc::nat => nat) n) s))
  3897                                   k))
  3898                            ((prob::((nat => bool) => bool) => real)
  3899                              (%s::nat => bool.
  3900                                  (op =::nat => nat => bool)
  3901                                   ((fst::nat * (nat => bool) => nat)
  3902                                     ((uniform::nat
  3903          => nat => (nat => bool) => nat * (nat => bool))
  3904 t ((Suc::nat => nat) n) s))
  3905                                   k'))))
  3906                        ((op ^::real => nat => real)
  3907                          ((op /::real => real => real) (1::real)
  3908                            ((number_of::bin => real)
  3909                              ((op BIT::bin => bool => bin)
  3910                                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3911                                  (True::bool))
  3912                                (False::bool))))
  3913                          t))))))"
  3914   by (import prob_uniform PROB_UNIFORM_PAIR_SUC)
  3915 
  3916 lemma PROB_UNIFORM_SUC: "(All::(nat => bool) => bool)
  3917  (%t::nat.
  3918      (All::(nat => bool) => bool)
  3919       (%n::nat.
  3920           (All::(nat => bool) => bool)
  3921            (%k::nat.
  3922                (op -->::bool => bool => bool)
  3923                 ((op <::nat => nat => bool) k ((Suc::nat => nat) n))
  3924                 ((op <=::real => real => bool)
  3925                   ((abs::real => real)
  3926                     ((op -::real => real => real)
  3927                       ((prob::((nat => bool) => bool) => real)
  3928                         (%s::nat => bool.
  3929                             (op =::nat => nat => bool)
  3930                              ((fst::nat * (nat => bool) => nat)
  3931                                ((uniform::nat
  3932     => nat => (nat => bool) => nat * (nat => bool))
  3933                                  t ((Suc::nat => nat) n) s))
  3934                              k))
  3935                       ((op /::real => real => real) (1::real)
  3936                         ((real::nat => real) ((Suc::nat => nat) n)))))
  3937                   ((op ^::real => nat => real)
  3938                     ((op /::real => real => real) (1::real)
  3939                       ((number_of::bin => real)
  3940                         ((op BIT::bin => bool => bin)
  3941                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3942                             (True::bool))
  3943                           (False::bool))))
  3944                     t)))))"
  3945   by (import prob_uniform PROB_UNIFORM_SUC)
  3946 
  3947 lemma PROB_UNIFORM: "(All::(nat => bool) => bool)
  3948  (%t::nat.
  3949      (All::(nat => bool) => bool)
  3950       (%n::nat.
  3951           (All::(nat => bool) => bool)
  3952            (%k::nat.
  3953                (op -->::bool => bool => bool)
  3954                 ((op <::nat => nat => bool) k n)
  3955                 ((op <=::real => real => bool)
  3956                   ((abs::real => real)
  3957                     ((op -::real => real => real)
  3958                       ((prob::((nat => bool) => bool) => real)
  3959                         (%s::nat => bool.
  3960                             (op =::nat => nat => bool)
  3961                              ((fst::nat * (nat => bool) => nat)
  3962                                ((uniform::nat
  3963     => nat => (nat => bool) => nat * (nat => bool))
  3964                                  t n s))
  3965                              k))
  3966                       ((op /::real => real => real) (1::real)
  3967                         ((real::nat => real) n))))
  3968                   ((op ^::real => nat => real)
  3969                     ((op /::real => real => real) (1::real)
  3970                       ((number_of::bin => real)
  3971                         ((op BIT::bin => bool => bin)
  3972                           ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
  3973                             (True::bool))
  3974                           (False::bool))))
  3975                     t)))))"
  3976   by (import prob_uniform PROB_UNIFORM)
  3977 
  3978 ;end_setup
  3979 
  3980 end
  3981