24 ((op &::bool => bool => bool) |
26 ((op &::bool => bool => bool) |
25 ((op =::nat => nat => bool) n |
27 ((op =::nat => nat => bool) n |
26 ((op +::nat => nat => nat) |
28 ((op +::nat => nat => nat) |
27 ((op *::nat => nat => nat) |
29 ((op *::nat => nat => nat) |
28 ((number_of::bin => nat) |
30 ((number_of::bin => nat) |
29 ((op BIT::bin => bool => bin) |
31 ((op BIT::bin => bit => bin) |
30 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
32 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
31 (True::bool)) |
33 (bit.B1::bit)) |
32 (False::bool))) |
34 (bit.B0::bit))) |
33 q) |
35 q) |
34 r)) |
36 r)) |
35 ((op |::bool => bool => bool) |
37 ((op |::bool => bool => bool) |
36 ((op =::nat => nat => bool) r (0::nat)) |
38 ((op =::nat => nat => bool) r (0::nat)) |
37 ((op =::nat => nat => bool) r (1::nat)))) |
39 ((op =::nat => nat => bool) r (1::nat)))) |
38 ((op &::bool => bool => bool) |
40 ((op &::bool => bool => bool) |
39 ((op =::nat => nat => bool) q |
41 ((op =::nat => nat => bool) q |
40 ((op div::nat => nat => nat) n |
42 ((op div::nat => nat => nat) n |
41 ((number_of::bin => nat) |
43 ((number_of::bin => nat) |
42 ((op BIT::bin => bool => bin) |
44 ((op BIT::bin => bit => bin) |
43 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
45 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
44 (True::bool)) |
46 (bit.B1::bit)) |
45 (False::bool))))) |
47 (bit.B0::bit))))) |
46 ((op =::nat => nat => bool) r |
48 ((op =::nat => nat => bool) r |
47 ((op mod::nat => nat => nat) n |
49 ((op mod::nat => nat => nat) n |
48 ((number_of::bin => nat) |
50 ((number_of::bin => nat) |
49 ((op BIT::bin => bool => bin) |
51 ((op BIT::bin => bit => bin) |
50 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
52 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
51 (True::bool)) |
53 (bit.B1::bit)) |
52 (False::bool)))))))))" |
54 (bit.B0::bit)))))))))" |
53 by (import prob_extra DIV_TWO_UNIQUE) |
55 by (import prob_extra DIV_TWO_UNIQUE) |
54 |
56 |
55 lemma DIVISION_TWO: "ALL n::nat. |
57 lemma DIVISION_TWO: "ALL n::nat. |
56 n = (2::nat) * (n div (2::nat)) + n mod (2::nat) & |
58 n = (2::nat) * (n div (2::nat)) + n mod (2::nat) & |
57 (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))" |
59 (n mod (2::nat) = (0::nat) | n mod (2::nat) = (1::nat))" |
73 (%n::nat. |
75 (%n::nat. |
74 (op -->::bool => bool => bool) |
76 (op -->::bool => bool => bool) |
75 ((op <::nat => nat => bool) |
77 ((op <::nat => nat => bool) |
76 ((op div::nat => nat => nat) m |
78 ((op div::nat => nat => nat) m |
77 ((number_of::bin => nat) |
79 ((number_of::bin => nat) |
78 ((op BIT::bin => bool => bin) |
80 ((op BIT::bin => bit => bin) |
79 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
81 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
80 (True::bool)) |
82 (bit.B1::bit)) |
81 (False::bool)))) |
83 (bit.B0::bit)))) |
82 ((op div::nat => nat => nat) n |
84 ((op div::nat => nat => nat) n |
83 ((number_of::bin => nat) |
85 ((number_of::bin => nat) |
84 ((op BIT::bin => bool => bin) |
86 ((op BIT::bin => bit => bin) |
85 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
87 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
86 (True::bool)) |
88 (bit.B1::bit)) |
87 (False::bool))))) |
89 (bit.B0::bit))))) |
88 ((op <::nat => nat => bool) m n)))" |
90 ((op <::nat => nat => bool) m n)))" |
89 by (import prob_extra DIV_TWO_MONO) |
91 by (import prob_extra DIV_TWO_MONO) |
90 |
92 |
91 lemma DIV_TWO_MONO_EVEN: "(All::(nat => bool) => bool) |
93 lemma DIV_TWO_MONO_EVEN: "(All::(nat => bool) => bool) |
92 (%m::nat. |
94 (%m::nat. |
95 (op -->::bool => bool => bool) ((EVEN::nat => bool) n) |
97 (op -->::bool => bool => bool) ((EVEN::nat => bool) n) |
96 ((op =::bool => bool => bool) |
98 ((op =::bool => bool => bool) |
97 ((op <::nat => nat => bool) |
99 ((op <::nat => nat => bool) |
98 ((op div::nat => nat => nat) m |
100 ((op div::nat => nat => nat) m |
99 ((number_of::bin => nat) |
101 ((number_of::bin => nat) |
100 ((op BIT::bin => bool => bin) |
102 ((op BIT::bin => bit => bin) |
101 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
103 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
102 (True::bool)) |
104 (bit.B1::bit)) |
103 (False::bool)))) |
105 (bit.B0::bit)))) |
104 ((op div::nat => nat => nat) n |
106 ((op div::nat => nat => nat) n |
105 ((number_of::bin => nat) |
107 ((number_of::bin => nat) |
106 ((op BIT::bin => bool => bin) |
108 ((op BIT::bin => bit => bin) |
107 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
109 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
108 (True::bool)) |
110 (bit.B1::bit)) |
109 (False::bool))))) |
111 (bit.B0::bit))))) |
110 ((op <::nat => nat => bool) m n))))" |
112 ((op <::nat => nat => bool) m n))))" |
111 by (import prob_extra DIV_TWO_MONO_EVEN) |
113 by (import prob_extra DIV_TWO_MONO_EVEN) |
112 |
114 |
113 lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n" |
115 lemma DIV_TWO_CANCEL: "ALL n. 2 * n div 2 = n & Suc (2 * n) div 2 = n" |
114 by (import prob_extra DIV_TWO_CANCEL) |
116 by (import prob_extra DIV_TWO_CANCEL) |
201 (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n) |
203 (op -->::bool => bool => bool) ((op <=::nat => nat => bool) m n) |
202 ((op <=::real => real => bool) |
204 ((op <=::real => real => bool) |
203 ((op ^::real => nat => real) |
205 ((op ^::real => nat => real) |
204 ((op /::real => real => real) (1::real) |
206 ((op /::real => real => real) (1::real) |
205 ((number_of::bin => real) |
207 ((number_of::bin => real) |
206 ((op BIT::bin => bool => bin) |
208 ((op BIT::bin => bit => bin) |
207 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
209 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
208 (True::bool)) |
210 (bit.B1::bit)) |
209 (False::bool)))) |
211 (bit.B0::bit)))) |
210 n) |
212 n) |
211 ((op ^::real => nat => real) |
213 ((op ^::real => nat => real) |
212 ((op /::real => real => real) (1::real) |
214 ((op /::real => real => real) (1::real) |
213 ((number_of::bin => real) |
215 ((number_of::bin => real) |
214 ((op BIT::bin => bool => bin) |
216 ((op BIT::bin => bit => bin) |
215 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
217 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
216 (True::bool)) |
218 (bit.B1::bit)) |
217 (False::bool)))) |
219 (bit.B0::bit)))) |
218 m))))" |
220 m))))" |
219 by (import prob_extra POW_HALF_MONO) |
221 by (import prob_extra POW_HALF_MONO) |
220 |
222 |
221 lemma POW_HALF_TWICE: "ALL n::nat. |
223 lemma POW_HALF_TWICE: "ALL n::nat. |
222 ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n" |
224 ((1::real) / (2::real)) ^ n = (2::real) * ((1::real) / (2::real)) ^ Suc n" |
2525 => (nat => bool) => bool) |
2527 => (nat => bool) => bool) |
2526 p (STL::(nat => bool) => nat => bool)))) |
2528 p (STL::(nat => bool) => nat => bool)))) |
2527 ((op *::real => real => real) |
2529 ((op *::real => real => real) |
2528 ((op /::real => real => real) (1::real) |
2530 ((op /::real => real => real) (1::real) |
2529 ((number_of::bin => real) |
2531 ((number_of::bin => real) |
2530 ((op BIT::bin => bool => bin) |
2532 ((op BIT::bin => bit => bin) |
2531 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
2533 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
2532 (True::bool)) |
2534 (bit.B1::bit)) |
2533 (False::bool)))) |
2535 (bit.B0::bit)))) |
2534 ((prob::((nat => bool) => bool) => real) p)))))" |
2536 ((prob::((nat => bool) => bool) => real) p)))))" |
2535 by (import prob PROB_INTER_SHD) |
2537 by (import prob PROB_INTER_SHD) |
2536 |
2538 |
2537 lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l" |
2539 lemma ALGEBRA_MEASURE_POS: "ALL l. 0 <= algebra_measure l" |
2538 by (import prob ALGEBRA_MEASURE_POS) |
2540 by (import prob ALGEBRA_MEASURE_POS) |
3153 x)))) |
3155 x)))) |
3154 ((op *::real => real => real) |
3156 ((op *::real => real => real) |
3155 ((op ^::real => nat => real) |
3157 ((op ^::real => nat => real) |
3156 ((op /::real => real => real) (1::real) |
3158 ((op /::real => real => real) (1::real) |
3157 ((number_of::bin => real) |
3159 ((number_of::bin => real) |
3158 ((op BIT::bin => bool => bin) |
3160 ((op BIT::bin => bit => bin) |
3159 ((op BIT::bin => bool => bin) |
3161 ((op BIT::bin => bit => bin) |
3160 (Numeral.Pls::bin) (True::bool)) |
3162 (Numeral.Pls::bin) (bit.B1::bit)) |
3161 (False::bool)))) |
3163 (bit.B0::bit)))) |
3162 ((size::bool list => nat) x)) |
3164 ((size::bool list => nat) x)) |
3163 ((prob::((nat => bool) => bool) => real) q))))))))" |
3165 ((prob::((nat => bool) => bool) => real) q))))))))" |
3164 by (import prob_indep INDEP_INDEP_SET_LEMMA) |
3166 by (import prob_indep INDEP_INDEP_SET_LEMMA) |
3165 |
3167 |
3166 lemma INDEP_SET_LIST: "(All::(((nat => bool) => bool) => bool) => bool) |
3168 lemma INDEP_SET_LIST: "(All::(((nat => bool) => bool) => bool) => bool) |
3379 ((All::(nat => bool) => bool) |
3381 ((All::(nat => bool) => bool) |
3380 (%v::nat. |
3382 (%v::nat. |
3381 (op -->::bool => bool => bool) |
3383 (op -->::bool => bool => bool) |
3382 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v) |
3384 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v) |
3383 ((number_of::bin => nat) |
3385 ((number_of::bin => nat) |
3384 ((op BIT::bin => bool => bin) |
3386 ((op BIT::bin => bit => bin) |
3385 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
3387 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3386 (True::bool)) |
3388 (bit.B1::bit)) |
3387 (False::bool))))) |
3389 (bit.B0::bit))))) |
3388 (P ((Suc::nat => nat) v))))) |
3390 (P ((Suc::nat => nat) v))))) |
3389 ((All::(nat => bool) => bool) P))" |
3391 ((All::(nat => bool) => bool) P))" |
3390 by (import prob_uniform unif_bound_ind) |
3392 by (import prob_uniform unif_bound_ind) |
3391 |
3393 |
3392 constdefs |
3394 constdefs |
3433 (All::((nat => bool) => bool) => bool) |
3435 (All::((nat => bool) => bool) => bool) |
3434 (%s::nat => bool. |
3436 (%s::nat => bool. |
3435 (op -->::bool => bool => bool) |
3437 (op -->::bool => bool => bool) |
3436 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2) |
3438 (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2) |
3437 ((number_of::bin => nat) |
3439 ((number_of::bin => nat) |
3438 ((op BIT::bin => bool => bin) |
3440 ((op BIT::bin => bit => bin) |
3439 ((op BIT::bin => bool => bin) |
3441 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3440 (Numeral.Pls::bin) (True::bool)) |
3442 (bit.B1::bit)) |
3441 (False::bool)))) |
3443 (bit.B0::bit)))) |
3442 s) |
3444 s) |
3443 (P ((Suc::nat => nat) v2) s))))) |
3445 (P ((Suc::nat => nat) v2) s))))) |
3444 ((All::(nat => bool) => bool) |
3446 ((All::(nat => bool) => bool) |
3445 (%v::nat. (All::((nat => bool) => bool) => bool) (P v))))" |
3447 (%v::nat. (All::((nat => bool) => bool) => bool) (P v))))" |
3446 by (import prob_uniform unif_ind) |
3448 by (import prob_uniform unif_ind) |
3713 (op -->::bool => bool => bool) |
3715 (op -->::bool => bool => bool) |
3714 ((Not::bool => bool) ((op =::nat => nat => bool) n (0::nat))) |
3716 ((Not::bool => bool) ((op =::nat => nat => bool) n (0::nat))) |
3715 ((op <=::nat => nat => bool) |
3717 ((op <=::nat => nat => bool) |
3716 ((op ^::nat => nat => nat) |
3718 ((op ^::nat => nat => nat) |
3717 ((number_of::bin => nat) |
3719 ((number_of::bin => nat) |
3718 ((op BIT::bin => bool => bin) |
3720 ((op BIT::bin => bit => bin) |
3719 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) |
3721 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) |
3720 (False::bool))) |
3722 (bit.B0::bit))) |
3721 ((unif_bound::nat => nat) n)) |
3723 ((unif_bound::nat => nat) n)) |
3722 ((op *::nat => nat => nat) |
3724 ((op *::nat => nat => nat) |
3723 ((number_of::bin => nat) |
3725 ((number_of::bin => nat) |
3724 ((op BIT::bin => bool => bin) |
3726 ((op BIT::bin => bit => bin) |
3725 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool)) |
3727 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit)) |
3726 (False::bool))) |
3728 (bit.B0::bit))) |
3727 n)))" |
3729 n)))" |
3728 by (import prob_uniform UNIF_BOUND_UPPER) |
3730 by (import prob_uniform UNIF_BOUND_UPPER) |
3729 |
3731 |
3730 lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)" |
3732 lemma UNIF_BOUND_UPPER_SUC: "ALL n. 2 ^ unif_bound n <= Suc (2 * n)" |
3731 by (import prob_uniform UNIF_BOUND_UPPER_SUC) |
3733 by (import prob_uniform UNIF_BOUND_UPPER_SUC) |
3768 (%k::nat. |
3770 (%k::nat. |
3769 (op -->::bool => bool => bool) |
3771 (op -->::bool => bool => bool) |
3770 ((op <=::nat => nat => bool) k |
3772 ((op <=::nat => nat => bool) k |
3771 ((op ^::nat => nat => nat) |
3773 ((op ^::nat => nat => nat) |
3772 ((number_of::bin => nat) |
3774 ((number_of::bin => nat) |
3773 ((op BIT::bin => bool => bin) |
3775 ((op BIT::bin => bit => bin) |
3774 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
3776 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3775 (True::bool)) |
3777 (bit.B1::bit)) |
3776 (False::bool))) |
3778 (bit.B0::bit))) |
3777 ((unif_bound::nat => nat) n))) |
3779 ((unif_bound::nat => nat) n))) |
3778 ((op =::real => real => bool) |
3780 ((op =::real => real => bool) |
3779 ((prob::((nat => bool) => bool) => real) |
3781 ((prob::((nat => bool) => bool) => real) |
3780 (%s::nat => bool. |
3782 (%s::nat => bool. |
3781 (op <::nat => nat => bool) |
3783 (op <::nat => nat => bool) |
3785 k)) |
3787 k)) |
3786 ((op *::real => real => real) ((real::nat => real) k) |
3788 ((op *::real => real => real) ((real::nat => real) k) |
3787 ((op ^::real => nat => real) |
3789 ((op ^::real => nat => real) |
3788 ((op /::real => real => real) (1::real) |
3790 ((op /::real => real => real) (1::real) |
3789 ((number_of::bin => real) |
3791 ((number_of::bin => real) |
3790 ((op BIT::bin => bool => bin) |
3792 ((op BIT::bin => bit => bin) |
3791 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
3793 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3792 (True::bool)) |
3794 (bit.B1::bit)) |
3793 (False::bool)))) |
3795 (bit.B0::bit)))) |
3794 ((unif_bound::nat => nat) n))))))" |
3796 ((unif_bound::nat => nat) n))))))" |
3795 by (import prob_uniform PROB_UNIF_BOUND) |
3797 by (import prob_uniform PROB_UNIF_BOUND) |
3796 |
3798 |
3797 lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)" |
3799 lemma PROB_UNIF_GOOD: "ALL n. 1 / 2 <= prob (%s. fst (unif n s) < Suc n)" |
3798 by (import prob_uniform PROB_UNIF_GOOD) |
3800 by (import prob_uniform PROB_UNIF_GOOD) |
3904 t ((Suc::nat => nat) n) s)) |
3906 t ((Suc::nat => nat) n) s)) |
3905 k')))) |
3907 k')))) |
3906 ((op ^::real => nat => real) |
3908 ((op ^::real => nat => real) |
3907 ((op /::real => real => real) (1::real) |
3909 ((op /::real => real => real) (1::real) |
3908 ((number_of::bin => real) |
3910 ((number_of::bin => real) |
3909 ((op BIT::bin => bool => bin) |
3911 ((op BIT::bin => bit => bin) |
3910 ((op BIT::bin => bool => bin) |
3912 ((op BIT::bin => bit => bin) |
3911 (Numeral.Pls::bin) (True::bool)) |
3913 (Numeral.Pls::bin) (bit.B1::bit)) |
3912 (False::bool)))) |
3914 (bit.B0::bit)))) |
3913 t))))))" |
3915 t))))))" |
3914 by (import prob_uniform PROB_UNIFORM_PAIR_SUC) |
3916 by (import prob_uniform PROB_UNIFORM_PAIR_SUC) |
3915 |
3917 |
3916 lemma PROB_UNIFORM_SUC: "(All::(nat => bool) => bool) |
3918 lemma PROB_UNIFORM_SUC: "(All::(nat => bool) => bool) |
3917 (%t::nat. |
3919 (%t::nat. |
3935 ((op /::real => real => real) (1::real) |
3937 ((op /::real => real => real) (1::real) |
3936 ((real::nat => real) ((Suc::nat => nat) n))))) |
3938 ((real::nat => real) ((Suc::nat => nat) n))))) |
3937 ((op ^::real => nat => real) |
3939 ((op ^::real => nat => real) |
3938 ((op /::real => real => real) (1::real) |
3940 ((op /::real => real => real) (1::real) |
3939 ((number_of::bin => real) |
3941 ((number_of::bin => real) |
3940 ((op BIT::bin => bool => bin) |
3942 ((op BIT::bin => bit => bin) |
3941 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
3943 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3942 (True::bool)) |
3944 (bit.B1::bit)) |
3943 (False::bool)))) |
3945 (bit.B0::bit)))) |
3944 t)))))" |
3946 t)))))" |
3945 by (import prob_uniform PROB_UNIFORM_SUC) |
3947 by (import prob_uniform PROB_UNIFORM_SUC) |
3946 |
3948 |
3947 lemma PROB_UNIFORM: "(All::(nat => bool) => bool) |
3949 lemma PROB_UNIFORM: "(All::(nat => bool) => bool) |
3948 (%t::nat. |
3950 (%t::nat. |
3966 ((op /::real => real => real) (1::real) |
3968 ((op /::real => real => real) (1::real) |
3967 ((real::nat => real) n)))) |
3969 ((real::nat => real) n)))) |
3968 ((op ^::real => nat => real) |
3970 ((op ^::real => nat => real) |
3969 ((op /::real => real => real) (1::real) |
3971 ((op /::real => real => real) (1::real) |
3970 ((number_of::bin => real) |
3972 ((number_of::bin => real) |
3971 ((op BIT::bin => bool => bin) |
3973 ((op BIT::bin => bit => bin) |
3972 ((op BIT::bin => bool => bin) (Numeral.Pls::bin) |
3974 ((op BIT::bin => bit => bin) (Numeral.Pls::bin) |
3973 (True::bool)) |
3975 (bit.B1::bit)) |
3974 (False::bool)))) |
3976 (bit.B0::bit)))) |
3975 t)))))" |
3977 t)))))" |
3976 by (import prob_uniform PROB_UNIFORM) |
3978 by (import prob_uniform PROB_UNIFORM) |
3977 |
3979 |
3978 ;end_setup |
3980 ;end_setup |
3979 |
3981 |