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