289 by (import prob_extra MAP_MEM) |
289 by (import prob_extra MAP_MEM) |
290 |
290 |
291 lemma MEM_NIL_MAP_CONS: "ALL (x::'a::type) l::'a::type list list. ~ [] mem map (op # x) l" |
291 lemma MEM_NIL_MAP_CONS: "ALL (x::'a::type) l::'a::type list list. ~ [] mem map (op # x) l" |
292 by (import prob_extra MEM_NIL_MAP_CONS) |
292 by (import prob_extra MEM_NIL_MAP_CONS) |
293 |
293 |
294 lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type:l. True] = l" |
294 lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type<-l. True] = l" |
295 by (import prob_extra FILTER_TRUE) |
295 by (import prob_extra FILTER_TRUE) |
296 |
296 |
297 lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type:l. False] = []" |
297 lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type<-l. False] = []" |
298 by (import prob_extra FILTER_FALSE) |
298 by (import prob_extra FILTER_FALSE) |
299 |
299 |
300 lemma FILTER_MEM: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list. |
300 lemma FILTER_MEM: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list. |
301 x mem filter P l --> P x" |
301 x mem filter P l --> P x" |
302 by (import prob_extra FILTER_MEM) |
302 by (import prob_extra FILTER_MEM) |
303 |
303 |
304 lemma MEM_FILTER: "ALL (P::'a::type => bool) (l::'a::type list) x::'a::type. |
304 lemma MEM_FILTER: "ALL (P::'a::type => bool) (l::'a::type list) x::'a::type. |
305 x mem filter P l --> x mem l" |
305 x mem filter P l --> x mem l" |
306 by (import prob_extra MEM_FILTER) |
306 by (import prob_extra MEM_FILTER) |
307 |
307 |
308 lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type:l. y ~= x] = l" |
308 lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type<-l. y ~= x] = l" |
309 by (import prob_extra FILTER_OUT_ELT) |
309 by (import prob_extra FILTER_OUT_ELT) |
310 |
310 |
311 lemma IS_PREFIX_NIL: "ALL x::'a::type list. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])" |
311 lemma IS_PREFIX_NIL: "ALL x::'a::type list. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])" |
312 by (import prob_extra IS_PREFIX_NIL) |
312 by (import prob_extra IS_PREFIX_NIL) |
313 |
313 |
1767 lemma ALG_COVER_UNIV: "alg_cover [[]] = K []" |
1767 lemma ALG_COVER_UNIV: "alg_cover [[]] = K []" |
1768 by (import prob_indep ALG_COVER_UNIV) |
1768 by (import prob_indep ALG_COVER_UNIV) |
1769 |
1769 |
1770 lemma MAP_CONS_TL_FILTER: "ALL (l::bool list list) b::bool. |
1770 lemma MAP_CONS_TL_FILTER: "ALL (l::bool list list) b::bool. |
1771 ~ [] mem l --> |
1771 ~ [] mem l --> |
1772 map (op # b) (map tl [x::bool list:l. hd x = b]) = |
1772 map (op # b) (map tl [x::bool list<-l. hd x = b]) = |
1773 [x::bool list:l. hd x = b]" |
1773 [x::bool list<-l. hd x = b]" |
1774 by (import prob_indep MAP_CONS_TL_FILTER) |
1774 by (import prob_indep MAP_CONS_TL_FILTER) |
1775 |
1775 |
1776 lemma ALG_COVER_SET_CASES_THM: "ALL l::bool list list. |
1776 lemma ALG_COVER_SET_CASES_THM: "ALL l::bool list list. |
1777 alg_cover_set l = |
1777 alg_cover_set l = |
1778 (l = [[]] | |
1778 (l = [[]] | |