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