1open List_conv; 2 3LIST_CONV (--`SNOC h []:'a list`--); 4LIST_CONV (--`SNOC h (CONS h t):'a list`--); 5 6LIST_CONV (--`NULL ([]:'a list)`--); 7LIST_CONV (--`NULL (CONS h t:'a list)`--); 8LIST_CONV (--`NULL (SNOC h t:'a list)`--); 9LIST_CONV (--`NULL (APPEND l1 l2 :'a list)`--); 10LIST_CONV (--`NULL [1;2;3]`--); 11LIST_CONV (--`NULL (REVERSE (l:bool list))`--); 12LIST_CONV (--`NULL (FLAT (l:'a list list))`--); 13 14LIST_CONV (--`LENGTH ([]:'a list)`--); 15LIST_CONV (--`LENGTH (CONS h t:'a list)`--); 16LIST_CONV (--`LENGTH (CONS h []:'a list)`--); 17LIST_CONV (--`LENGTH (SNOC h t:'a list)`--); 18LIST_CONV (--`LENGTH (SNOC h []:'a list)`--); 19LIST_CONV (--`LENGTH (APPEND l1 l2 :'a list)`--); 20LIST_CONV (--`LENGTH [1;2;3]`--); 21LIST_CONV (--`LENGTH (SNOC 1 (SNOC 2 (SNOC 3 [])))`--); 22LIST_CONV (--`LENGTH (FLAT (l :num list list))`--); 23LIST_CONV (--`LENGTH (FLAT (l :'a list list))`--); 24 25LIST_CONV (--`MAP (P:'a list -> 'a) []`--); 26LIST_CONV (--`MAP (P:'a list -> 'a) (CONS h t)`--); 27LIST_CONV (--`MAP (P:'a list -> 'a) (CONS h [])`--); 28LIST_CONV (--`MAP (P:'a list -> 'a) (SNOC h t)`--); 29LIST_CONV (--`MAP (P:'a list -> 'a) (SNOC h [])`--); 30LIST_CONV (--`MAP (P:'a list -> 'a) [x;y;z]`--); 31LIST_CONV (--`MAP (P:num list ->num) (APPEND l1 l2)`--); 32LIST_CONV (--`MAP (f:'a ->'b) (FLAT l)`--); 33LIST_CONV (--`MAP (f:num ->num) (FLAT l)`--); 34 35LIST_CONV (--`FILTER (g:'b ->bool) []`--); 36LIST_CONV (--`FILTER (g:'b ->bool) (CONS h t)`--); 37LIST_CONV (--`FILTER (g:'b ->bool) (SNOC h t)`--); 38LIST_CONV (--`FILTER (P:num list -> bool) (APPEND l1 l2)`--); 39LIST_CONV (--`FILTER (f:'a -> bool) (FLAT l)`--); 40 41LIST_CONV (--`APPEND (l1:'a list) []`--); 42LIST_CONV (--`APPEND [] (l1:'a list)`--); 43LIST_CONV (--`APPEND (l1:'a list) (CONS h t)`--); 44(* LIST_CONV (--`APPEND (l1:'a list) (APPEND l2 l3)`--) 45 handle e => Raise e; BLOCKED *) 46LIST_CONV (--`APPEND (APPEND l2 l3)(l1:'a list)`--); 47LIST_CONV (--`APPEND (l1:'a list) (SNOC h t)`--); 48(* LIST_CONV (--`APPEND (SNOC h t) (l1:'a list)`--) 49 handle e => Raise e; BLOCKED *) 50LIST_CONV (--`APPEND [1;2;3] [4;5;6]`--); 51LIST_CONV (--`APPEND (SNOC 1 (SNOC 2 (SNOC 3 []))) [4;5;6]`--); 52LIST_CONV (--`APPEND [4;5;6] (SNOC 1 (SNOC 2 (SNOC 3 [])))`--); 53LIST_CONV (--`APPEND [x] (l1:'a list)`--); 54LIST_CONV (--`APPEND (CONS h t) ((CONS h t):'a list)`--); 55LIST_CONV (--`APPEND (CONS h1 t1) ((SNOC h2 t2):'a list)`--); 56LIST_CONV (--`APPEND (CONS h t) (l1:'a list)`--); 57LIST_CONV (--`APPEND (l1:'a list) (CONS h t)`--); 58 59LIST_CONV (--`FLAT (CONS h t :'a list list)`--); 60LIST_CONV (--`FLAT (SNOC h t :'a list list)`--); 61LIST_CONV (--`FLAT ([] :'a list list)`--); 62LIST_CONV (--`FLAT (FLAT (l :'a list list list))`--); 63LIST_CONV (--`FLAT (APPEND l1 l2 :'a list list)`--); 64LIST_CONV (--`FLAT ([[h]] :'a list list)`--); 65 66LIST_CONV (--`ALL_EL P ([]:'a list)`--); 67LIST_CONV (--`ALL_EL P (CONS h t:'a list)`--); 68LIST_CONV (--`ALL_EL P (SNOC h t:'a list)`--); 69LIST_CONV (--`ALL_EL P (APPEND l1 l2:'a list)`--); 70LIST_CONV (--`ALL_EL P (REVERSE (l:num list))`--); 71LIST_CONV (--`ALL_EL P (FLAT (l:'a list list))`--); 72 73LIST_CONV (--`SOME_EL P ([]:'a list)`--); 74LIST_CONV (--`SOME_EL P (CONS h t:'a list)`--); 75LIST_CONV (--`SOME_EL P (SNOC h t:'a list)`--); 76LIST_CONV (--`SOME_EL P (APPEND l1 l2:'a list)`--); 77LIST_CONV (--`SOME_EL P (REVERSE (l:'a list))`--); 78LIST_CONV (--`SOME_EL P (FLAT (l:'a list list))`--); 79 80LIST_CONV (--`IS_EL P ([]:'a list)`--); 81LIST_CONV (--`IS_EL P (CONS h t:'a list)`--); 82LIST_CONV (--`IS_EL P (SNOC h t:'a list)`--); 83LIST_CONV (--`IS_EL P (APPEND l1 l2:'a list)`--); 84LIST_CONV (--`IS_EL x (REVERSE (l:'a list))`--); 85LIST_CONV (--`IS_EL P (FLAT (l:'a list list))`--); 86 87LIST_CONV (--`SUM []`--); 88LIST_CONV (--`SUM (CONS h t)`--); 89LIST_CONV (--`SUM (SNOC h t)`--); 90LIST_CONV (--`SUM (APPEND l1 l2)`--); 91LIST_CONV (--`SUM (REVERSE (l:num list))`--); 92LIST_CONV (--`SUM (FLAT l)`--); 93 94LIST_CONV (--`AND_EL []`--); 95LIST_CONV (--`AND_EL (CONS h t)`--); 96LIST_CONV (--`AND_EL (SNOC h t)`--); 97LIST_CONV (--`AND_EL (APPEND l1 l2)`--); 98LIST_CONV (--`AND_EL (REVERSE l)`--); 99LIST_CONV (--`AND_EL (FLAT l)`--); 100 101LIST_CONV (--`OR_EL []`--); 102LIST_CONV (--`OR_EL (CONS h t)`--); 103LIST_CONV (--`OR_EL (SNOC h t)`--); 104LIST_CONV (--`OR_EL (APPEND l1 l2)`--); 105LIST_CONV (--`OR_EL (REVERSE l)`--); 106LIST_CONV (--`OR_EL (FLAT l)`--); 107 108 109LIST_CONV (--`REVERSE ([]:'a list)`--); 110LIST_CONV (--`REVERSE (CONS h t:'a list)`--); 111LIST_CONV (--`REVERSE (SNOC h t:'a list)`--); 112LIST_CONV (--`REVERSE (APPEND l1 l2:'a list)`--); 113LIST_CONV (--`REVERSE (FLAT l:'a list list)`--); 114 115LIST_CONV (--`PREFIX P ([]:'a list)`--); 116LIST_CONV (--`PREFIX P (CONS x l:'a list)`--); 117 118LIST_CONV (--`SUFFIX P ([]:'a list)`--); 119LIST_CONV (--`SUFFIX P (SNOC x l:'a list)`--); 120 121LIST_CONV (--`(FLAT o REVERSE) ([]:'a list list)`--); 122LIST_CONV (--`(FLAT o REVERSE) (CONS x l:'a list list)`--); 123LIST_CONV (--`(FLAT o REVERSE) (APPEND l1 l2:'a list list)`--); 124LIST_CONV (--`(FLAT o REVERSE) (FLAT l:'a list list)`--); 125 126val db = list_thm_database (); 127 128val COMM_ADD = prove((--`COMM $+`--), 129 REWRITE_TAC[definition "operator" "COMM_DEF"] THEN 130 REPEAT GEN_TAC THEN 131 SUBST1_TAC(SPECL[(--`x:num`--),(--`y:num`--)] 132 (theorem "arithmetic" "ADD_SYM")) THEN 133 REWRITE_TAC[]); 134 135val ASSOC_DEF = definition "operator" "ASSOC_DEF"; 136val RIGHT_ID_DEF = definition "operator" "RIGHT_ID_DEF"; 137val LEFT_ID_DEF = definition "operator" "LEFT_ID_DEF"; 138val MONOID_DEF = definition "operator" "MONOID_DEF"; 139 140val ADD_SYM = theorem "arithmetic" "ADD_SYM"; 141val ADD_ASSOC = theorem "arithmetic" "ADD_ASSOC"; 142val ADD = definition "arithmetic" "ADD"; 143val ADD_CLAUSES = theorem "arithmetic" "ADD_CLAUSES"; 144 145val ASSOC_ADD = TAC_PROOF(([], --`ASSOC $+`--), 146 REWRITE_TAC[ASSOC_DEF,ADD_ASSOC]); 147 148val RIGHT_ID_ADD_0 = TAC_PROOF(([], --`RIGHT_ID $+ 0`--), 149 REWRITE_TAC[RIGHT_ID_DEF,ADD_CLAUSES]); 150 151val LEFT_ID_ADD_0 = TAC_PROOF(([], --`LEFT_ID $+ 0`--), 152 REWRITE_TAC[LEFT_ID_DEF,ADD_CLAUSES]); 153 154val MONOID_ADD_0 = TAC_PROOF(([], --`MONOID $+ 0`--), 155 REWRITE_TAC[MONOID_DEF,ASSOC_ADD, 156 LEFT_ID_ADD_0,RIGHT_ID_ADD_0]); 157 158 159set_list_thm_database 160 {Fold_thms =[theorem "List" "SUM_FOLDR", theorem "List" "SUM_FOLDL"], 161 Aux_thms = [MONOID_ADD_0, COMM_ADD]}; 162 163LIST_CONV (--`SUM []`--); 164LIST_CONV (--`SUM (CONS h t)`--); 165LIST_CONV (--`SUM (SNOC h t)`--); 166LIST_CONV (--`SUM (APPEND l1 l2)`--); 167LIST_CONV (--`SUM (REVERSE (l:num list))`--); 168LIST_CONV (--`SUM (FLAT l)`--); 169 170set_list_thm_database {Fold_thms = [], Aux_thms = []}; 171 172X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []} 173 (--`SUM []`--); 174X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []} 175 (--`SUM (CONS h t)`--); 176X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDL"], Aux_thms = []} 177 (--`SUM (SNOC h t)`--); 178X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], 179 Aux_thms = [MONOID_ADD_0]} 180 (--`SUM (APPEND l1 l2)`--); 181X_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], 182 Aux_thms = [MONOID_ADD_0]} 183 (--`SUM (FLAT l)`--); 184 185 186set_list_thm_database(db); 187 188LIST_CONV (--`SUM []`--); 189LIST_CONV (--`SUM (CONS h t)`--); 190LIST_CONV (--`SUM (SNOC h t)`--); 191LIST_CONV (--`SUM (APPEND l1 l2)`--); 192LIST_CONV (--`SUM (REVERSE (l:num list))`--); 193LIST_CONV (--`SUM (FLAT l)`--); 194 195 196PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []} 197 (--`SUM []`--); 198PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], Aux_thms = []} 199 (--`SUM (CONS h t)`--); 200PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDL"], Aux_thms = []} 201 (--`SUM (SNOC h t)`--); 202PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], 203 Aux_thms = [MONOID_ADD_0]} 204 (--`SUM (APPEND l1 l2)`--); 205PURE_LIST_CONV {Fold_thms = [theorem "List" "SUM_FOLDR"], 206 Aux_thms = [MONOID_ADD_0]} 207 (--`SUM (FLAT l)`--); 208 209 210 211 212 213 214(* 215new_theory "foo"; 216val MULTL_FOLDR = new_definition ("MULTL_FOLDR", 217 (--`MULTL l = FOLDR $* 1 l`--) 218 ); 219val MULTL_FOLDL = new_definition ("MULTL_FOLDL", 220 (--`MULTL_FOLDL l = FOLDL $* 1 l`--) 221 ); 222 223?? ML type errors 224LIST_CONV ([MULTL_FOLDR], []) (--`MULTL []`--); 225LIST_CONV ([MULTL_FOLDR], []) (--`MULTL (CONS h t)`--); 226LIST_CONV ([MULTL_FOLDL], []) (--`MULTL_FOLDL (SNOC h t)`--); 227*) 228 229 230 231(* EVALUATION CONVERSIONS *) 232 233SUM_CONV (--`SUM []`--); 234SUM_CONV (--`SUM [1]`--); 235SUM_CONV (--`SUM [1;2;3;4]`--); 236 237 238EL_CONV (--`EL 0 ([]:num list)`--); 239EL_CONV (--`EL 0 [0]`--); 240EL_CONV (--`EL 0 [0;1;2;3]`--); 241EL_CONV (--`EL 1 [0;1;2;3]`--); 242EL_CONV (--`EL 3 [0;1;2;3]`--); 243EL_CONV (--`EL 3 [T;F;F;T]`--); 244 245ELL_CONV (--`ELL 0 ([0]:num list)`--); 246ELL_CONV (--`ELL 0 ([0;1;2;3]:num list)`--); 247ELL_CONV (--`ELL 1 ([0;1;2;3]:num list)`--); 248ELL_CONV (--`ELL 3 ([0;1;2;3]:num list)`--); 249ELL_CONV (--`ELL 3 [T;F;F;T]`--); 250 251FLAT_CONV (--`FLAT [[1;2;3;4];[2;3;4];[3;4]]`--); 252FLAT_CONV (--`FLAT [[];[];([]:'a list)]`--); 253FLAT_CONV (--`FLAT [[];[1];[]]`--); 254 255APPEND_CONV (--`APPEND [1;2;3;4] [2;3;4]`--); 256 257LENGTH_CONV (--`LENGTH [1;2;3;4]`--); 258REVERSE_CONV(--`REVERSE [1;2;3;4]`--); 259REVERSE_CONV(--`REVERSE [1]`--); 260REVERSE_CONV(--`REVERSE ([]:'a list)`--); 261 262SNOC_CONV(--`SNOC 5 []`--); 263SNOC_CONV(--`SNOC 5 [1;2;3;4]`--); 264 265LAST_CONV (--`LAST [1;2;3;4]`--); 266BUTLAST_CONV (--`BUTLAST [1;2;3;4]`--); 267 268SEG_CONV (--`SEG 2 3 [0;1;2;3;4;5;6]`--); 269SEG_CONV (--`SEG 4 3 [0;1;2;3;4;5;6]`--); 270SEG_CONV (--`SEG 4 0 [0;1;2;3;4;5;6]`--); 271 272REPLICATE_CONV (--`REPLICATE 4 4`--); 273REPLICATE_CONV (--`REPLICATE 0 4`--); 274 275REPLICATE_CONV (--`REPLICATE 3 (x:bool)`--); 276REPLICATE_CONV (--`REPLICATE 3 (SUC 3)`--); 277REPLICATE_CONV (--`REPLICATE 3 T`--); 278REPLICATE_CONV (--`REPLICATE 3 (1 + (2+ 3))`--); 279REPLICATE_CONV (--`REPLICATE 3 [1;2;3]`--); 280REPLICATE_CONV (--`REPLICATE 0 [1;2;3]`--); 281 282 283FIRSTN_CONV(--`FIRSTN 2 [1;2;3;4]`--); 284FIRSTN_CONV(--`FIRSTN 3 [1;2;3;4]`--); 285 286BUTLASTN_CONV (--`BUTLASTN 2 [1;2;3;4]`--); 287 288BUTFIRSTN_CONV (--`BUTFIRSTN 2 [1;2;3;4]`--); 289 290LASTN_CONV (--`LASTN 2 [1;2;3;4]`--); 291LASTN_CONV (--`LASTN 1 [1;2;3;4]`--); 292 293MAP_CONV LENGTH_CONV (--`MAP LENGTH [[1;2;3;4];[2;3;4];[3;4]]`--); 294 295FOLDR_CONV APPEND_CONV (--`FOLDR APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--); 296FOLDL_CONV APPEND_CONV (--`FOLDL APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--); 297 298GENLIST_CONV (BETA_CONV THENC (TOP_DEPTH_CONV num_CONV)) 299 (--`GENLIST (\n . SUC n) 4`--); 300 301SCANL_CONV APPEND_CONV (--`SCANL APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--); 302SCANR_CONV APPEND_CONV (--`SCANR APPEND [] [[1;2;3;4];[2;3;4];[3;4]]`--); 303 304MAP2_CONV APPEND_CONV 305 (--`MAP2 APPEND [[1;2;3;4];[2;3;4];[3;4]] [[1;2;3;4];[2;3;4];[3;4]]`--); 306 307FILTER_CONV BETA_CONV (--`FILTER (\x. T) [1;2;3;4]`--); 308FILTER_CONV BETA_CONV (--`FILTER (\x. F) [1;2;3;4]`--); 309 310ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. F) [1;2;3;4]`--); 311ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. T) [1;2;3;4]`--); 312ALL_EL_CONV BETA_CONV (--`ALL_EL (\x. T) ([]:num list)`--); 313ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = F) [T;T;F;F]`--); 314ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = T) [T;T;F;F]`--); 315ALL_EL_CONV (BETA_CONV THENC bool_EQ_CONV) (--`ALL_EL (\x. x = T) [T;T;T]`--); 316 317SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. F) [1;2;3;4]`--); 318SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. T) [1;2;3;4]`--); 319SOME_EL_CONV BETA_CONV (--`SOME_EL (\x. T) ([]:num list)`--); 320 321IS_EL_CONV bool_EQ_CONV (--`IS_EL T [F;F;F;F]`--); 322IS_EL_CONV bool_EQ_CONV (--`IS_EL F [T;T;F;F]`--); 323IS_EL_CONV bool_EQ_CONV (--`IS_EL F []`--); 324 325AND_EL_CONV (--`AND_EL []`--); 326AND_EL_CONV (--`AND_EL [T]`--); 327AND_EL_CONV (--`AND_EL [F]`--); 328AND_EL_CONV (--`AND_EL [T;F;T;F]`--); 329AND_EL_CONV (--`AND_EL [F;F;F;F]`--); 330 331OR_EL_CONV (--`OR_EL []`--); 332OR_EL_CONV (--`OR_EL [T]`--); 333OR_EL_CONV (--`OR_EL [F]`--); 334OR_EL_CONV (--`OR_EL [T;F;T;F]`--); 335OR_EL_CONV (--`OR_EL [F;F;F;F]`--); 336 337 338(* 339NULL_CONV (--`NULL ([]:'a list)`--); 340NULL_CONV (--`NULL [T]`--); 341NULL_CONV (--`NULL [1;2;3]`--); 342NULL_CONV (--`NULL [[1;2;3];[1]]`--); 343 344HD_CONV (--`HD [1]`--); 345HD_CONV (--`HD [1;2;3]`--); 346 347TL_CONV (--`TL [1]`--); 348TL_CONV (--`TL [1;2;3]`--); 349*) 350 351 352list_EQ_CONV bool_EQ_CONV (--`[] = ([]:bool list)`--); 353list_EQ_CONV bool_EQ_CONV (--`[T] = [F]`--); 354list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [F;T;F;F]`--); 355 356list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [F]`--); (* FAILS *) 357list_EQ_CONV bool_EQ_CONV (--`[T;F;T;F] = [T;F;T]`--); (* FAILS *) 358list_EQ_CONV bool_EQ_CONV (--`[T] = []`--); (* FAILS *) 359list_EQ_CONV bool_EQ_CONV (--`[] = [T]`--); (* FAILS *) 360 361(* 362g `!l. APPEND [1] l = CONS 1 l`; 363e SNOC_INDUCT_TAC; 364b(); 365e LIST_INDUCT_TAC; 366 367g `!l1 l2.( LENGTH l1 = LENGTH l2) ==> (APPEND [1] l1 = CONS 1 l2)`; 368e EQ_LENGTH_INDUCT_TAC; 369b(); 370e EQ_LENGTH_SNOC_INDUCT_TAC; 371*) 372 373 374(* (KLS) The following is unnecessary, since "define_type" has not been 375 changed. But anyway, we'll leave it. 376 377new_theory "temp"; 378 379val void_Axiom = define_type{name="void_Axiom" , 380 type_spec= `void = Void`, 381 fixities = [Prefix]}; 382 383val pair = define_type{name="pair", 384 type_spec= `pair = CONST of 'a#'b`, 385 fixities = [Prefix]}; 386 387val onetest = define_type{name="onetest", 388 type_spec=`onetest = OOOO of one`, 389 fixities = [Prefix]}; 390 391val tri_Axiom = define_type{name="tri_Axiom", 392 type_spec=`tri = Hi | Lo | Fl`, 393 fixities = [Prefix,Prefix,Prefix]}; 394 395val iso_Axiom = define_type{name="iso_Axiom", 396 type_spec=`iso = ISO of 'a`, 397 fixities = [Prefix]}; 398 399val List_Axiom = define_type{name="List_Axiom", 400 type_spec=`List = Nil | CCC of 'a => List`, 401 fixities = [Prefix,Infix 40]}; 402 403val ty_Axiom = define_type{name="ty_Axiom", 404 type_spec = `ty = C1 of 'a 405 | C2 406 | C3 of 'a => 'b => ty 407 | C4 of ty => 'c => ty => 'a => 'b 408 | C5 of ty => ty`, 409 fixities = [Prefix, Prefix, Prefix, Prefix, Prefix]}; 410 411define_type{name="bintree", 412 type_spec=`bintree = LEAF of 'a 413 | TREE of bintree => bintree`, 414 fixities = [Prefix,Prefix]}; 415 416define_type{name="seven", 417 type_spec= `typ = C of one 418 => (one#one) 419 => (one -> one-> 'a list) 420 => ('a,one#one,'a list) ty`, 421 fixities = [Prefix]}; 422 423define_type{name="seven'", 424 type_spec= `Typ = D of one # (one#one) # (one -> one -> 'a list) 425 # ('a,one#one,'a list) ty`, 426 fixities = [Prefix]}; 427*) 428