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