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