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