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