35 lemma DIV_TWO_BASIC: "(op &::bool => bool => bool) |
35 lemma DIV_TWO_BASIC: "(op &::bool => bool => bool) |
36 ((op =::nat => nat => bool) |
36 ((op =::nat => nat => bool) |
37 ((op div::nat => nat => nat) (0::nat) |
37 ((op div::nat => nat => nat) (0::nat) |
38 ((number_of \<Colon> int => nat) |
38 ((number_of \<Colon> int => nat) |
39 ((op BIT \<Colon> int => bit => int) |
39 ((op BIT \<Colon> int => bit => int) |
40 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
40 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
41 (bit.B0::bit)))) |
41 (bit.B0::bit)))) |
42 (0::nat)) |
42 (0::nat)) |
43 ((op &::bool => bool => bool) |
43 ((op &::bool => bool => bool) |
44 ((op =::nat => nat => bool) |
44 ((op =::nat => nat => bool) |
45 ((op div::nat => nat => nat) (1::nat) |
45 ((op div::nat => nat => nat) (1::nat) |
46 ((number_of \<Colon> int => nat) |
46 ((number_of \<Colon> int => nat) |
47 ((op BIT \<Colon> int => bit => int) |
47 ((op BIT \<Colon> int => bit => int) |
48 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
48 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
49 (bit.B0::bit)))) |
49 (bit.B0::bit)))) |
50 (0::nat)) |
50 (0::nat)) |
51 ((op =::nat => nat => bool) |
51 ((op =::nat => nat => bool) |
52 ((op div::nat => nat => nat) |
52 ((op div::nat => nat => nat) |
53 ((number_of \<Colon> int => nat) |
53 ((number_of \<Colon> int => nat) |
54 ((op BIT \<Colon> int => bit => int) |
54 ((op BIT \<Colon> int => bit => int) |
55 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
55 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
56 (bit.B0::bit))) |
56 (bit.B0::bit))) |
57 ((number_of \<Colon> int => nat) |
57 ((number_of \<Colon> int => nat) |
58 ((op BIT \<Colon> int => bit => int) |
58 ((op BIT \<Colon> int => bit => int) |
59 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
59 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
60 (bit.B0::bit)))) |
60 (bit.B0::bit)))) |
61 (1::nat)))" |
61 (1::nat)))" |
62 by (import prob_extra DIV_TWO_BASIC) |
62 by (import prob_extra DIV_TWO_BASIC) |
63 |
63 |
64 lemma DIV_TWO_MONO: "ALL (m::nat) n::nat. m div 2 < n div 2 --> m < n" |
64 lemma DIV_TWO_MONO: "ALL (m::nat) n::nat. m div 2 < n div 2 --> m < n" |
75 (op =::nat => nat => bool) |
75 (op =::nat => nat => bool) |
76 ((op div::nat => nat => nat) |
76 ((op div::nat => nat => nat) |
77 ((op ^::nat => nat => nat) |
77 ((op ^::nat => nat => nat) |
78 ((number_of \<Colon> int => nat) |
78 ((number_of \<Colon> int => nat) |
79 ((op BIT \<Colon> int => bit => int) |
79 ((op BIT \<Colon> int => bit => int) |
80 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
80 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
81 (bit.B0::bit))) |
81 (bit.B0::bit))) |
82 ((Suc::nat => nat) n)) |
82 ((Suc::nat => nat) n)) |
83 ((number_of \<Colon> int => nat) |
83 ((number_of \<Colon> int => nat) |
84 ((op BIT \<Colon> int => bit => int) |
84 ((op BIT \<Colon> int => bit => int) |
85 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
85 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
86 (bit.B0::bit)))) |
86 (bit.B0::bit)))) |
87 ((op ^::nat => nat => nat) |
87 ((op ^::nat => nat => nat) |
88 ((number_of \<Colon> int => nat) |
88 ((number_of \<Colon> int => nat) |
89 ((op BIT \<Colon> int => bit => int) |
89 ((op BIT \<Colon> int => bit => int) |
90 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
90 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
91 (bit.B0::bit))) |
91 (bit.B0::bit))) |
92 n))" |
92 n))" |
93 by (import prob_extra EXP_DIV_TWO) |
93 by (import prob_extra EXP_DIV_TWO) |
94 |
94 |
95 lemma EVEN_EXP_TWO: "ALL n::nat. EVEN (2 ^ n) = (n ~= 0)" |
95 lemma EVEN_EXP_TWO: "ALL n::nat. EVEN (2 ^ n) = (n ~= 0)" |
125 |
125 |
126 lemma HALF_POS: "(op <::real => real => bool) (0::real) |
126 lemma HALF_POS: "(op <::real => real => bool) (0::real) |
127 ((op /::real => real => real) (1::real) |
127 ((op /::real => real => real) (1::real) |
128 ((number_of \<Colon> int => real) |
128 ((number_of \<Colon> int => real) |
129 ((op BIT \<Colon> int => bit => int) |
129 ((op BIT \<Colon> int => bit => int) |
130 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
130 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
131 (bit.B0::bit))))" |
131 (bit.B0::bit))))" |
132 by (import prob_extra HALF_POS) |
132 by (import prob_extra HALF_POS) |
133 |
133 |
134 lemma HALF_CANCEL: "(op =::real => real => bool) |
134 lemma HALF_CANCEL: "(op =::real => real => bool) |
135 ((op *::real => real => real) |
135 ((op *::real => real => real) |
136 ((number_of \<Colon> int => real) |
136 ((number_of \<Colon> int => real) |
137 ((op BIT \<Colon> int => bit => int) |
137 ((op BIT \<Colon> int => bit => int) |
138 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
138 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
139 (bit.B0::bit))) |
139 (bit.B0::bit))) |
140 ((op /::real => real => real) (1::real) |
140 ((op /::real => real => real) (1::real) |
141 ((number_of \<Colon> int => real) |
141 ((number_of \<Colon> int => real) |
142 ((op BIT \<Colon> int => bit => int) |
142 ((op BIT \<Colon> int => bit => int) |
143 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
143 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
144 (bit.B0::bit))))) |
144 (bit.B0::bit))))) |
145 (1::real)" |
145 (1::real)" |
146 by (import prob_extra HALF_CANCEL) |
146 by (import prob_extra HALF_CANCEL) |
147 |
147 |
148 lemma POW_HALF_POS: "(All::(nat => bool) => bool) |
148 lemma POW_HALF_POS: "(All::(nat => bool) => bool) |
150 (op <::real => real => bool) (0::real) |
150 (op <::real => real => bool) (0::real) |
151 ((op ^::real => nat => real) |
151 ((op ^::real => nat => real) |
152 ((op /::real => real => real) (1::real) |
152 ((op /::real => real => real) (1::real) |
153 ((number_of \<Colon> int => real) |
153 ((number_of \<Colon> int => real) |
154 ((op BIT \<Colon> int => bit => int) |
154 ((op BIT \<Colon> int => bit => int) |
155 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
155 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
156 (bit.B0::bit)))) |
156 (bit.B0::bit)))) |
157 n))" |
157 n))" |
158 by (import prob_extra POW_HALF_POS) |
158 by (import prob_extra POW_HALF_POS) |
159 |
159 |
160 lemma POW_HALF_MONO: "(All::(nat => bool) => bool) |
160 lemma POW_HALF_MONO: "(All::(nat => bool) => bool) |
165 ((op <=::real => real => bool) |
165 ((op <=::real => real => bool) |
166 ((op ^::real => nat => real) |
166 ((op ^::real => nat => real) |
167 ((op /::real => real => real) (1::real) |
167 ((op /::real => real => real) (1::real) |
168 ((number_of \<Colon> int => real) |
168 ((number_of \<Colon> int => real) |
169 ((op BIT \<Colon> int => bit => int) |
169 ((op BIT \<Colon> int => bit => int) |
170 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
170 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
171 (bit.B1::bit)) |
171 (bit.B1::bit)) |
172 (bit.B0::bit)))) |
172 (bit.B0::bit)))) |
173 n) |
173 n) |
174 ((op ^::real => nat => real) |
174 ((op ^::real => nat => real) |
175 ((op /::real => real => real) (1::real) |
175 ((op /::real => real => real) (1::real) |
176 ((number_of \<Colon> int => real) |
176 ((number_of \<Colon> int => real) |
177 ((op BIT \<Colon> int => bit => int) |
177 ((op BIT \<Colon> int => bit => int) |
178 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
178 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
179 (bit.B1::bit)) |
179 (bit.B1::bit)) |
180 (bit.B0::bit)))) |
180 (bit.B0::bit)))) |
181 m))))" |
181 m))))" |
182 by (import prob_extra POW_HALF_MONO) |
182 by (import prob_extra POW_HALF_MONO) |
183 |
183 |
186 (op =::real => real => bool) |
186 (op =::real => real => bool) |
187 ((op ^::real => nat => real) |
187 ((op ^::real => nat => real) |
188 ((op /::real => real => real) (1::real) |
188 ((op /::real => real => real) (1::real) |
189 ((number_of \<Colon> int => real) |
189 ((number_of \<Colon> int => real) |
190 ((op BIT \<Colon> int => bit => int) |
190 ((op BIT \<Colon> int => bit => int) |
191 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
191 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
192 (bit.B0::bit)))) |
192 (bit.B0::bit)))) |
193 n) |
193 n) |
194 ((op *::real => real => real) |
194 ((op *::real => real => real) |
195 ((number_of \<Colon> int => real) |
195 ((number_of \<Colon> int => real) |
196 ((op BIT \<Colon> int => bit => int) |
196 ((op BIT \<Colon> int => bit => int) |
197 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
197 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
198 (bit.B0::bit))) |
198 (bit.B0::bit))) |
199 ((op ^::real => nat => real) |
199 ((op ^::real => nat => real) |
200 ((op /::real => real => real) (1::real) |
200 ((op /::real => real => real) (1::real) |
201 ((number_of \<Colon> int => real) |
201 ((number_of \<Colon> int => real) |
202 ((op BIT \<Colon> int => bit => int) |
202 ((op BIT \<Colon> int => bit => int) |
203 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
203 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
204 (bit.B1::bit)) |
204 (bit.B1::bit)) |
205 (bit.B0::bit)))) |
205 (bit.B0::bit)))) |
206 ((Suc::nat => nat) n))))" |
206 ((Suc::nat => nat) n))))" |
207 by (import prob_extra POW_HALF_TWICE) |
207 by (import prob_extra POW_HALF_TWICE) |
208 |
208 |
227 lemma ONE_MINUS_HALF: "(op =::real => real => bool) |
227 lemma ONE_MINUS_HALF: "(op =::real => real => bool) |
228 ((op -::real => real => real) (1::real) |
228 ((op -::real => real => real) (1::real) |
229 ((op /::real => real => real) (1::real) |
229 ((op /::real => real => real) (1::real) |
230 ((number_of \<Colon> int => real) |
230 ((number_of \<Colon> int => real) |
231 ((op BIT \<Colon> int => bit => int) |
231 ((op BIT \<Colon> int => bit => int) |
232 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
232 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
233 (bit.B0::bit))))) |
233 (bit.B0::bit))))) |
234 ((op /::real => real => real) (1::real) |
234 ((op /::real => real => real) (1::real) |
235 ((number_of \<Colon> int => real) |
235 ((number_of \<Colon> int => real) |
236 ((op BIT \<Colon> int => bit => int) |
236 ((op BIT \<Colon> int => bit => int) |
237 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
237 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
238 (bit.B0::bit))))" |
238 (bit.B0::bit))))" |
239 by (import prob_extra ONE_MINUS_HALF) |
239 by (import prob_extra ONE_MINUS_HALF) |
240 |
240 |
241 lemma HALF_LT_1: "(op <::real => real => bool) |
241 lemma HALF_LT_1: "(op <::real => real => bool) |
242 ((op /::real => real => real) (1::real) |
242 ((op /::real => real => real) (1::real) |
243 ((number_of \<Colon> int => real) |
243 ((number_of \<Colon> int => real) |
244 ((op BIT \<Colon> int => bit => int) |
244 ((op BIT \<Colon> int => bit => int) |
245 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
245 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
246 (bit.B0::bit)))) |
246 (bit.B0::bit)))) |
247 (1::real)" |
247 (1::real)" |
248 by (import prob_extra HALF_LT_1) |
248 by (import prob_extra HALF_LT_1) |
249 |
249 |
250 lemma POW_HALF_EXP: "(All::(nat => bool) => bool) |
250 lemma POW_HALF_EXP: "(All::(nat => bool) => bool) |
252 (op =::real => real => bool) |
252 (op =::real => real => bool) |
253 ((op ^::real => nat => real) |
253 ((op ^::real => nat => real) |
254 ((op /::real => real => real) (1::real) |
254 ((op /::real => real => real) (1::real) |
255 ((number_of \<Colon> int => real) |
255 ((number_of \<Colon> int => real) |
256 ((op BIT \<Colon> int => bit => int) |
256 ((op BIT \<Colon> int => bit => int) |
257 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
257 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
258 (bit.B0::bit)))) |
258 (bit.B0::bit)))) |
259 n) |
259 n) |
260 ((inverse::real => real) |
260 ((inverse::real => real) |
261 ((real::nat => real) |
261 ((real::nat => real) |
262 ((op ^::nat => nat => nat) |
262 ((op ^::nat => nat => nat) |
263 ((number_of \<Colon> int => nat) |
263 ((number_of \<Colon> int => nat) |
264 ((op BIT \<Colon> int => bit => int) |
264 ((op BIT \<Colon> int => bit => int) |
265 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
265 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
266 (bit.B1::bit)) |
266 (bit.B1::bit)) |
267 (bit.B0::bit))) |
267 (bit.B0::bit))) |
268 n))))" |
268 n))))" |
269 by (import prob_extra POW_HALF_EXP) |
269 by (import prob_extra POW_HALF_EXP) |
270 |
270 |
1405 ((op +::real => real => real) |
1405 ((op +::real => real => real) |
1406 ((op ^::real => nat => real) |
1406 ((op ^::real => nat => real) |
1407 ((op /::real => real => real) (1::real) |
1407 ((op /::real => real => real) (1::real) |
1408 ((number_of \<Colon> int => real) |
1408 ((number_of \<Colon> int => real) |
1409 ((op BIT \<Colon> int => bit => int) |
1409 ((op BIT \<Colon> int => bit => int) |
1410 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
1410 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
1411 (bit.B1::bit)) |
1411 (bit.B1::bit)) |
1412 (bit.B0::bit)))) |
1412 (bit.B0::bit)))) |
1413 ((size::bool list => nat) |
1413 ((size::bool list => nat) |
1414 ((SNOC::bool => bool list => bool list) (True::bool) l))) |
1414 ((SNOC::bool => bool list => bool list) (True::bool) l))) |
1415 ((op ^::real => nat => real) |
1415 ((op ^::real => nat => real) |
1416 ((op /::real => real => real) (1::real) |
1416 ((op /::real => real => real) (1::real) |
1417 ((number_of \<Colon> int => real) |
1417 ((number_of \<Colon> int => real) |
1418 ((op BIT \<Colon> int => bit => int) |
1418 ((op BIT \<Colon> int => bit => int) |
1419 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) |
1419 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) |
1420 (bit.B1::bit)) |
1420 (bit.B1::bit)) |
1421 (bit.B0::bit)))) |
1421 (bit.B0::bit)))) |
1422 ((size::bool list => nat) |
1422 ((size::bool list => nat) |
1423 ((SNOC::bool => bool list => bool list) (False::bool) l)))) |
1423 ((SNOC::bool => bool list => bool list) (False::bool) l)))) |
1424 ((op ^::real => nat => real) |
1424 ((op ^::real => nat => real) |
1425 ((op /::real => real => real) (1::real) |
1425 ((op /::real => real => real) (1::real) |
1426 ((number_of \<Colon> int => real) |
1426 ((number_of \<Colon> int => real) |
1427 ((op BIT \<Colon> int => bit => int) |
1427 ((op BIT \<Colon> int => bit => int) |
1428 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit)) |
1428 ((op BIT \<Colon> int => bit => int) (Int.Pls \<Colon> int) (bit.B1::bit)) |
1429 (bit.B0::bit)))) |
1429 (bit.B0::bit)))) |
1430 ((size::bool list => nat) l)))" |
1430 ((size::bool list => nat) l)))" |
1431 by (import prob ALG_TWINS_MEASURE) |
1431 by (import prob ALG_TWINS_MEASURE) |
1432 |
1432 |
1433 lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 & |
1433 lemma ALG_MEASURE_BASIC: "alg_measure [] = 0 & |