1open HolKernel boolLib bossLib Parse; 2open EmitML combinTheory pairTheory numeralTheory whileTheory arithmeticTheory; 3open pred_setTheory optionTheory basicSizeTheory listTheory rich_listTheory; 4open stringTheory sumTheory finite_mapTheory sortingTheory; 5open bitTheory numeral_bitTheory fcpTheory fcpLib wordsTheory 6open integerTheory integer_wordTheory intSyntax; 7open numposrepTheory ASCIInumbersTheory 8 9val _ = new_theory "basis_emit"; 10 11(* == Combin ============================================================== *) 12 13val defs = map DEFN [S_THM, K_THM, I_THM, W_THM, C_THM, o_THM, APPLY_UPDATE_THM] 14 15val _ = eSML "combin" defs; 16val _ = eCAML "combin" defs; 17 18(* == Pair ================================================================ *) 19 20val defs = 21 map EmitML.DEFN [CURRY_DEF,UNCURRY_DEF,FST,SND,PAIR_MAP_THM,LEX_DEF_THM]; 22 23val _ = eSML "pair" defs; 24val _ = eCAML "pair" defs; 25 26val B = PP.block PP.CONSISTENT 0 27val S = PP.add_string 28val NL = PP.NL 29val _ = adjoin_to_theory 30 {sig_ps = NONE, 31 struct_ps = SOME ( 32 fn _ => 33 B [S "val _ = ConstMapML.insert pairSyntax.comma_tm;", NL] 34 )}; 35 36(* == Num ================================================================= *) 37 38val addition_thms = 39 let val thms = List.take(CONJUNCTS(SPEC_ALL numeral_add), 6) 40 in REWRITE_RULE [iZ] (LIST_CONJ thms) 41 end; 42 43val T_INTRO = Q.prove(`!x. x = (x = T)`, REWRITE_TAC []); 44val F_INTRO = Q.prove(`!x. ~x = (x = F)`, REWRITE_TAC []); 45 46val (even,odd) = 47 let val [a,b,c,d,e,f] = CONJUNCTS (SPEC_ALL numeral_evenodd) 48 val [a',b',f'] = map (PURE_ONCE_REWRITE_RULE [T_INTRO]) [a,b,f] 49 val [c',d',e'] = map (PURE_REWRITE_RULE [F_INTRO]) [c,d,e] 50 in 51 (LIST_CONJ [a',b',c'], LIST_CONJ [d',e',f']) 52 end; 53 54val DIV_FAIL = Q.prove 55(`!m. m DIV ZERO = FAIL $DIV ^(mk_var("zero denominator",bool)) m ZERO`, 56REWRITE_TAC [combinTheory.FAIL_THM]); 57 58val MOD_FAIL = Q.prove 59(`!m. m MOD ZERO = FAIL $MOD ^(mk_var("zero denominator",bool)) m ZERO`, 60REWRITE_TAC [combinTheory.FAIL_THM]); 61 62val (div_eqns, mod_eqns) = 63 let val [a,b,c,d] = CONJUNCTS DIVMOD_NUMERAL_CALC 64 in (CONJ DIV_FAIL (CONJ a b), 65 CONJ MOD_FAIL (CONJ c d)) 66 end; 67 68val _ = 69 ConstMapML.prim_insert (Term.prim_mk_const{Name="0",Thy="num"}, 70 (true,"num","ZERO",Type.mk_type("num",[]))); 71 72val defs = map DEFN 73 [numeral_suc,iZ,iiSUC,addition_thms, 74 numeral_lt, numeral_lte,GREATER_DEF,GREATER_OR_EQ, 75 numeral_pre,iDUB_removal,iSUB_THM, numeral_sub, 76 numeral_mult,iSQR,numeral_exp,even,odd, 77 numeral_fact,numeral_funpow,numeral_MIN,numeral_MAX, 78 WHILE,LEAST_DEF,REWRITE_RULE [TIMES2,GSYM iDUB] findq_thm, 79 DIVMOD_THM,div_eqns, mod_eqns, 80 numeral_div2,REWRITE_RULE [iMOD_2EXP] numeral_imod_2exp,DIV_2EXP, 81 prim_recTheory.measure_thm] 82 83val _ = EmitML.reshape_thm_hook := 84 (Rewrite.PURE_REWRITE_RULE [arithmeticTheory.NUMERAL_DEF] o 85 !EmitML.reshape_thm_hook); 86 87val _ = eSML "num" 88 (EQDATATYPE ([], `num = ZERO | BIT1 num | BIT2 num`) 89 :: OPEN ["combin"] 90 :: MLSTRUCT "val num_size = I" (* Not sure this is needed *) 91 :: MLSTRUCT "fun NUMERAL x = x" (* Not sure this is needed *) 92 :: MLSTRUCT "val ONE = BIT1 ZERO" 93 :: (defs @ 94 [MLSIG "val num_size : num -> num", 95 MLSIG "val NUMERAL :num -> num", 96 MLSIG "val ZERO :num", 97 MLSIG "val BIT1 :num -> num", 98 MLSIG "val BIT2 :num -> num", 99 MLSIG "val ONE :num", 100 MLSIG "val TWO :num", 101 MLSIG "val fromInt : int -> num", 102 MLSIG "val toInt : num -> int option", 103 MLSIG "val toBinString : num -> string", 104 MLSIG "val toOctString : num -> string", 105 MLSIG "val toDecString : num -> string", 106 MLSIG "val toHexString : num -> string", 107 MLSIG "val toString : num -> string", 108 MLSIG "val fromBinString : string -> num", 109 MLSIG "val fromOctString : string -> num", 110 MLSIG "val fromDecString : string -> num", 111 MLSIG "val fromHexString : string -> num", 112 MLSIG "val fromString : string -> num", 113 MLSIG "val ppBin : num PP.pprinter", 114 MLSIG "val ppOct : num PP.pprinter", 115 MLSIG "val ppDec : num PP.pprinter", 116 MLSIG "val ppHex : num PP.pprinter", 117 MLSIG "val pp_num : num PP.pprinter", 118 MLSTRUCT "\n\ 119\ (*---------------------------------------------------------------------------*)\n\ 120\ (* Supplementary ML, not generated from HOL theorems, aimed at supporting *)\n\ 121\ (* parsing and pretty printing of numerals. *)\n\ 122\ (*---------------------------------------------------------------------------*)\n\ 123\ \n\ 124\ val TWO = BIT2 ZERO;\n\ 125\ val THREE = BIT1 (BIT1 ZERO);\n\ 126\ val FOUR = BIT2 (BIT1 ZERO);\n\ 127\ val EIGHT = BIT2(BIT1(BIT1 ZERO));\n\ 128\ val TEN = BIT2(BIT2(BIT1 ZERO));\n\ 129\ val SIXTEEN = BIT2(BIT1(BIT1(BIT1 ZERO)));\n\ 130\\n\ 131\\n\ 132\ fun toBaseString divmod_b d n =\n\ 133\ let fun toBaseStr n s =\n\ 134\ if n = ZERO then\n\ 135\ if s = \"\" then \"0\" else s\n\ 136\ else let val (q, r) = divmod_b n in\n\ 137\ toBaseStr q (^(str (d r), s))\n\ 138\ end\n\ 139\ in\n\ 140\ toBaseStr n \"\"\n\ 141\ end\n\ 142\\n\ 143\ fun BIN ZERO = #\"0\"\n\ 144\ | BIN (BIT1 ZERO) = #\"1\"\n\ 145\ | BIN otherwise = #\"?\";\n\ 146\\n\ 147\ fun UNBIN #\"0\" = ZERO\n\ 148\ | UNBIN #\"1\" = BIT1 ZERO\n\ 149\ | UNBIN other = raise Fail \"not a binary character\";\n\ 150\\n\ 151\ fun OCT ZERO = #\"0\"\n\ 152\ | OCT (BIT1 ZERO) = #\"1\"\n\ 153\ | OCT (BIT2 ZERO) = #\"2\"\n\ 154\ | OCT (BIT1(BIT1 ZERO)) = #\"3\"\n\ 155\ | OCT (BIT2(BIT1 ZERO)) = #\"4\"\n\ 156\ | OCT (BIT1(BIT2 ZERO)) = #\"5\"\n\ 157\ | OCT (BIT2(BIT2 ZERO)) = #\"6\"\n\ 158\ | OCT (BIT1(BIT1(BIT1 ZERO))) = #\"7\"\n\ 159\ | OCT otherwise = #\"?\";\n\ 160\\n\ 161\ fun UNOCT #\"0\" = ZERO\n\ 162\ | UNOCT #\"1\" = BIT1 ZERO\n\ 163\ | UNOCT #\"2\" = BIT2 ZERO\n\ 164\ | UNOCT #\"3\" = BIT1(BIT1 ZERO)\n\ 165\ | UNOCT #\"4\" = BIT2(BIT1 ZERO)\n\ 166\ | UNOCT #\"5\" = BIT1(BIT2 ZERO)\n\ 167\ | UNOCT #\"6\" = BIT2(BIT2 ZERO)\n\ 168\ | UNOCT #\"7\" = BIT1(BIT1(BIT1 ZERO))\n\ 169\ | UNOCT other = raise Fail \"not an octal character\";\n\ 170\\n\ 171\\n\ 172\ fun DIGIT ZERO = #\"0\"\n\ 173\ | DIGIT (BIT1 ZERO) = #\"1\"\n\ 174\ | DIGIT (BIT2 ZERO) = #\"2\"\n\ 175\ | DIGIT (BIT1(BIT1 ZERO)) = #\"3\"\n\ 176\ | DIGIT (BIT2(BIT1 ZERO)) = #\"4\"\n\ 177\ | DIGIT (BIT1(BIT2 ZERO)) = #\"5\"\n\ 178\ | DIGIT (BIT2(BIT2 ZERO)) = #\"6\"\n\ 179\ | DIGIT (BIT1(BIT1(BIT1 ZERO))) = #\"7\"\n\ 180\ | DIGIT (BIT2(BIT1(BIT1 ZERO))) = #\"8\"\n\ 181\ | DIGIT (BIT1(BIT2(BIT1 ZERO))) = #\"9\"\n\ 182\ | DIGIT otherwise = #\"?\";\n\ 183\\n\ 184\ fun UNDIGIT #\"0\" = ZERO\n\ 185\ | UNDIGIT #\"1\" = BIT1 ZERO\n\ 186\ | UNDIGIT #\"2\" = BIT2 ZERO\n\ 187\ | UNDIGIT #\"3\" = BIT1(BIT1 ZERO)\n\ 188\ | UNDIGIT #\"4\" = BIT2(BIT1 ZERO)\n\ 189\ | UNDIGIT #\"5\" = BIT1(BIT2 ZERO)\n\ 190\ | UNDIGIT #\"6\" = BIT2(BIT2 ZERO)\n\ 191\ | UNDIGIT #\"7\" = BIT1(BIT1(BIT1 ZERO))\n\ 192\ | UNDIGIT #\"8\" = BIT2(BIT1(BIT1 ZERO))\n\ 193\ | UNDIGIT #\"9\" = BIT1(BIT2(BIT1 ZERO))\n\ 194\ | UNDIGIT other = raise Fail \"not a decimal character\";\n\ 195\\n\ 196\ fun HEX ZERO = #\"0\"\n\ 197\ | HEX (BIT1 ZERO) = #\"1\"\n\ 198\ | HEX (BIT2 ZERO) = #\"2\"\n\ 199\ | HEX (BIT1(BIT1 ZERO)) = #\"3\"\n\ 200\ | HEX (BIT2(BIT1 ZERO)) = #\"4\"\n\ 201\ | HEX (BIT1(BIT2 ZERO)) = #\"5\"\n\ 202\ | HEX (BIT2(BIT2 ZERO)) = #\"6\"\n\ 203\ | HEX (BIT1(BIT1(BIT1 ZERO))) = #\"7\"\n\ 204\ | HEX (BIT2(BIT1(BIT1 ZERO))) = #\"8\"\n\ 205\ | HEX (BIT1(BIT2(BIT1 ZERO))) = #\"9\"\n\ 206\ | HEX (BIT2(BIT2(BIT1 ZERO))) = #\"A\"\n\ 207\ | HEX (BIT1(BIT1(BIT2 ZERO))) = #\"B\"\n\ 208\ | HEX (BIT2(BIT1(BIT2 ZERO))) = #\"C\"\n\ 209\ | HEX (BIT1(BIT2(BIT2 ZERO))) = #\"D\"\n\ 210\ | HEX (BIT2(BIT2(BIT2 ZERO))) = #\"E\"\n\ 211\ | HEX (BIT1(BIT1(BIT1(BIT1 ZERO)))) = #\"F\"\n\ 212\ | HEX otherwise = #\"?\";\n\ 213\\n\ 214\ fun UNHEX #\"0\" = ZERO\n\ 215\ | UNHEX #\"1\" = BIT1 ZERO\n\ 216\ | UNHEX #\"2\" = BIT2 ZERO\n\ 217\ | UNHEX #\"3\" = BIT1(BIT1 ZERO)\n\ 218\ | UNHEX #\"4\" = BIT2(BIT1 ZERO)\n\ 219\ | UNHEX #\"5\" = BIT1(BIT2 ZERO)\n\ 220\ | UNHEX #\"6\" = BIT2(BIT2 ZERO)\n\ 221\ | UNHEX #\"7\" = BIT1(BIT1(BIT1 ZERO))\n\ 222\ | UNHEX #\"8\" = BIT2(BIT1(BIT1 ZERO))\n\ 223\ | UNHEX #\"9\" = BIT1(BIT2(BIT1 ZERO))\n\ 224\ | UNHEX #\"a\" = BIT2(BIT2(BIT1 ZERO))\n\ 225\ | UNHEX #\"A\" = BIT2(BIT2(BIT1 ZERO))\n\ 226\ | UNHEX #\"b\" = BIT1(BIT1(BIT2 ZERO))\n\ 227\ | UNHEX #\"B\" = BIT1(BIT1(BIT2 ZERO))\n\ 228\ | UNHEX #\"c\" = BIT2(BIT1(BIT2 ZERO))\n\ 229\ | UNHEX #\"C\" = BIT2(BIT1(BIT2 ZERO))\n\ 230\ | UNHEX #\"d\" = BIT1(BIT2(BIT2 ZERO))\n\ 231\ | UNHEX #\"D\" = BIT1(BIT2(BIT2 ZERO))\n\ 232\ | UNHEX #\"e\" = BIT2(BIT2(BIT2 ZERO))\n\ 233\ | UNHEX #\"E\" = BIT2(BIT2(BIT2 ZERO))\n\ 234\ | UNHEX #\"f\" = BIT1(BIT1(BIT1(BIT1 ZERO)))\n\ 235\ | UNHEX #\"F\" = BIT1(BIT1(BIT1(BIT1 ZERO)))\n\ 236\ | UNHEX other = raise Fail \"not a hex character\";\n\ 237\\n\ 238\\n\ 239\ val toBinString = toBaseString (fn n => (DIV2 n, MOD_2EXP ONE n)) BIN;\n\ 240\ fun fromBinString dstr =\n\ 241\ let val nlist = List.map UNBIN (String.explode dstr)\n\ 242\ in\n\ 243\ List.foldl (fn (a,b) => + a ( * b TWO)) (hd nlist) (tl nlist)\n\ 244\ end;\n\ 245\\n\ 246\ val toDecString = toBaseString (fn n => DIVMOD(ZERO, (n, TEN))) DIGIT;\n\ 247\ fun fromDecString dstr =\n\ 248\ let val nlist = List.map UNDIGIT (String.explode dstr)\n\ 249\ in\n\ 250\ List.foldl (fn (a,b) => + a ( * b TEN)) (hd nlist) (tl nlist)\n\ 251\ end;\n\ 252\\n\ 253\ val toOctString = toBaseString\n\ 254\ (fn n => (DIV2 (DIV2 (DIV2 n)), MOD_2EXP THREE n)) OCT;\n\ 255\ fun fromOctString dstr =\n\ 256\ let val nlist = List.map UNOCT (String.explode dstr)\n\ 257\ in\n\ 258\ List.foldl (fn (a,b) => + a ( * b EIGHT)) (hd nlist) (tl nlist)\n\ 259\ end;\n\ 260\\n\ 261\ val toHexString = toBaseString\n\ 262\ (fn n => (DIV2 (DIV2 (DIV2 (DIV2 n))), MOD_2EXP FOUR n)) HEX;\n\ 263\ fun fromHexString dstr =\n\ 264\ let val nlist = List.map UNHEX (String.explode dstr)\n\ 265\ in\n\ 266\ List.foldl (fn (a,b) => + a ( * b SIXTEEN)) (hd nlist) (tl nlist)\n\ 267\ end;\n\ 268\\n\ 269\ (* Uncomment to add mappings to portableML/Arbnum.sml (+ add to signature)\n\ 270\\n\ 271\ fun Arbnum2num m =\n\ 272\ if m = Arbnum.zero then ZERO else\n\ 273\ let val n = Arbnum2num (Arbnum.div2 m) in\n\ 274\ if Arbnum.mod2 m = Arbnum.zero then\n\ 275\ iDUB n\n\ 276\ else\n\ 277\ BIT1 n\n\ 278\ end\n\ 279\\n\ 280\ fun num2Arbnum ZERO = Arbnum.zero\n\ 281\ | num2Arbnum (BIT1 n) = Arbnum.plus1(Arbnum.times2(num2Arbnum n))\n\ 282\ | num2Arbnum (BIT2 n) = Arbnum.plus2(Arbnum.times2(num2Arbnum n))\n\ 283\\n\ 284\ fun toDecString n = Arbnum.toString (num2Arbnum n);\n\ 285\ *)\n\ 286\\n\ 287\ (* Installed in MoscowML with Meta.installPP *)\n\ 288\\n\ 289\ fun ppBin n = PP.add_string (toBinString n);\n\ 290\ fun ppOct n = PP.add_string (toOctString n);\n\ 291\ fun ppDec n = PP.add_string (toDecString n);\n\ 292\ fun ppHex n = PP.add_string (toHexString n);\n\ 293\ val toString = toDecString;\n\ 294\ val fromString = fromDecString;\n\ 295\ val pp_num = ppHex;\n\ 296\\n\ 297\ fun fromInt i = fromDecString (Int.toString i)\n\ 298\ fun toInt n =\n\ 299\ let fun num2int ZERO = 0\n\ 300\ | num2int (BIT1 n) = Int.+(Int.*(2, num2int n), 1)\n\ 301\ | num2int (BIT2 n) = Int.+(Int.*(2, num2int n), 2)\n\ 302\ in\n\ 303\ SOME (num2int n) handle Overflow => NONE\n\ 304\ end;\n\n"])); 305 306val _ = eCAML "num" 307 (DATATYPE (`num = ZERO | BIT1 num | BIT2 num`) 308 :: map MLSTRUCT 309 ["let num_size x = x", 310 "let _NUMERAL x = x", 311 "let _ONE = BIT1 ZERO", 312 "let _TWO = BIT2 ZERO"] 313 @ defs 314 @ map MLSIG 315 ["val num_size : num -> num", 316 "val _NUMERAL : num -> num", 317 "val _ONE : num", 318 "val _TWO : num", 319 "val int_of_holnum : num -> int", 320 "val holnum_of_int : int -> num", 321 "val big_int_of_holnum : num -> Big_int.big_int", 322 "val holnum_of_big_int : Big_int.big_int -> num", 323 "val fromString : string -> num", 324 "val toString : num -> string"] 325 @ map MLSTRUCT 326 ["", 327 "let rec int_of_holnum n = match n with\n\ 328 \ ZERO -> 0\n\ 329 \ | BIT1 x -> succ ((int_of_holnum x) lsl 1)\n\ 330 \ | BIT2 x -> Pervasives.(+) ((int_of_holnum x) lsl 1) 2", 331 "", 332 "let rec holnum_of_int n =\n\ 333 \ if n = 0 then ZERO\n\ 334 \ else let q = n / 2 and r = n mod 2 in\n\ 335 \ let m = holnum_of_int q in\n\ 336 \ if r = 0 then iDUB m else BIT1 m", "", 337 "let rec big_int_of_holnum n = match n with\n\ 338 \ ZERO -> Big_int.zero_big_int\n\ 339 \ | BIT1 x -> Big_int.succ_big_int\n\ 340 \ (Big_int.mult_int_big_int 2 (big_int_of_holnum x))\n\ 341 \ | BIT2 x -> Big_int.add_int_big_int 2\n\ 342 \ (Big_int.mult_int_big_int 2 (big_int_of_holnum x))", "", 343 "let rec holnum_of_big_int n =\n\ 344 \ if Big_int.eq_big_int n Big_int.zero_big_int then ZERO\n\ 345 \ else let (q,r) = Big_int.quomod_big_int n\ 346 \ (Big_int.big_int_of_int 2) in\n\ 347 \ let m = holnum_of_big_int q in\n\ 348 \ if Big_int.eq_big_int r Big_int.zero_big_int then\ 349 \ iDUB m else BIT1 m", "", 350 "let fromString s = holnum_of_big_int (Big_int.big_int_of_string s)", 351 "let toString n = Big_int.string_of_big_int (big_int_of_holnum n)"]); 352 353(*---------------------------------------------------------------------------*) 354(* Map 0 and ZERO to the same thing in generated ML. *) 355(*---------------------------------------------------------------------------*) 356val _ = adjoin_to_theory 357{sig_ps = NONE, struct_ps = SOME (fn _ => 358 B [S "val _ = ConstMapML.prim_insert ", NL, 359 S " (Term.prim_mk_const{Name=\"0\",Thy=\"num\"},", NL, 360 S " (true,\"num\",\"ZERO\",Type.mk_type(\"num\",[])));",NL])}; 361 362(*---------------------------------------------------------------------------*) 363(* Automatic rewrite for definitions *) 364(*---------------------------------------------------------------------------*) 365 366val _ = adjoin_to_theory {sig_ps = NONE, 367 struct_ps = SOME (fn _ => 368 B[S "val _ = EmitML.reshape_thm_hook := ", NL, 369 S " (Rewrite.PURE_REWRITE_RULE [arithmeticTheory.NUMERAL_DEF] o ", 370 NL, S " !EmitML.reshape_thm_hook);", NL, NL])} 371 372 373(* == Set ================================================================= *) 374 375(*---------------------------------------------------------------------------*) 376(* Export an ML model of (finite) sets. Although the representation used in *) 377(* pred_set is 'a -> bool, the ML representation is a concrete type with *) 378(* constructors EMPTY and INSERT. Which is quite different, but we wanted to *) 379(* be able to compute cardinality, which would not be possible with sets-as- *) 380(* predicates. An alternative would be to have a parallel theory of finite *) 381(* sets, as in hol88, but that could lead to a proliferation of theories *) 382(* which required sets. *) 383(* *) 384(* The implementation is not efficient. Insertion is constant time, but *) 385(* membership checks are linear and subset checks are quadratic. *) 386(*---------------------------------------------------------------------------*) 387 388fun TAKE2 l = case List.take(l, 2) of [a,b] => (a,b) 389 | _ => raise (mk_HOL_ERR "emitCAML" "TAKE2" "Not three elements"); 390 391val TAKE2_CONJUNCTS = TAKE2 o CONJUNCTS; 392 393val F_INTRO = PURE_REWRITE_RULE [PROVE[] (Term `~x = (x = F)`)]; 394val T_INTRO = PURE_ONCE_REWRITE_RULE [PROVE[] (Term `x = (x = T)`)]; 395 396val BIGINTER_EMPTY = Q.prove 397(`BIGINTER EMPTY = FAIL BIGINTER ^(mk_var("empty set",bool)) EMPTY`, 398 REWRITE_TAC [combinTheory.FAIL_THM]); 399 400val MIN_SET_EMPTY = Q.prove 401(`MIN_SET EMPTY = FAIL MIN_SET ^(mk_var("empty set",bool)) EMPTY`, 402 REWRITE_TAC [combinTheory.FAIL_THM]); 403 404val (tyg,tmg) = (type_grammar(),term_grammar()) 405val tyg' = type_grammar.remove_abbreviation tyg "set" 406val _ = temp_set_grammars(tyg',tmg) 407val _ = new_type("set",1) 408val _ = temp_clear_overloads_on "set" 409 410val IS_EMPTY_def = Define`IS_EMPTY s = if s = {} then T else F` 411val IS_EMPTY_THM = Q.prove 412(`(IS_EMPTY {} = T) /\ (IS_EMPTY (x INSERT s) = F)`, 413 SRW_TAC[][IS_EMPTY_def]) 414val IS_EMPTY_REWRITE = store_thm( 415"IS_EMPTY_REWRITE", 416``((s = {}) = IS_EMPTY s) /\ (({} = s) = IS_EMPTY s)``, 417SRW_TAC[][EQ_IMP_THM,IS_EMPTY_def]) 418 419val defs = 420 map DEFN_NOSIG [CONJ (F_INTRO NOT_IN_EMPTY) IN_INSERT, 421 CONJ (CONJUNCT1 UNION_EMPTY) INSERT_UNION, 422 CONJ (CONJUNCT1 INTER_EMPTY) INSERT_INTER, 423 CONJ EMPTY_DELETE DELETE_INSERT, CONJ DIFF_EMPTY DIFF_INSERT, 424 CONJ (T_INTRO (SPEC_ALL EMPTY_SUBSET)) INSERT_SUBSET, PSUBSET_EQN, 425 CONJ IMAGE_EMPTY IMAGE_INSERT, CONJ BIGUNION_EMPTY BIGUNION_INSERT, 426 LIST_CONJ [BIGINTER_EMPTY,BIGINTER_SING, BIGINTER_INSERT], 427 CONJ CARD_EMPTY (UNDISCH (SPEC_ALL CARD_INSERT)), 428 CONJ (T_INTRO (CONJUNCT1 (SPEC_ALL DISJOINT_EMPTY))) DISJOINT_INSERT, 429 CROSS_EQNS, 430 listTheory.LIST_TO_SET_THM, IS_EMPTY_THM, 431 let val (c1,c2) = TAKE2_CONJUNCTS (SPEC_ALL SUM_IMAGE_THM) 432 in CONJ c1 (UNDISCH (SPEC_ALL c2)) end, 433 let val (c1,c2) = TAKE2_CONJUNCTS SUM_SET_THM 434 in CONJ c1 (UNDISCH (SPEC_ALL c2)) end, 435 let val (c1,c2) = TAKE2_CONJUNCTS MAX_SET_THM 436 in CONJ c1 (UNDISCH (SPEC_ALL c2)) end, 437 CONJ MIN_SET_EMPTY MIN_SET_THM, count_EQN,POW_EQNS]; 438 439val _ = eSML "set" 440 (ABSDATATYPE (["'a"], `set = EMPTY | INSERT 'a set`) 441 :: OPEN ["num"] 442 :: MLSIG "type num = numML.num" 443 :: MLSIG "val EMPTY : 'a set" 444 :: MLSIG "val INSERT : 'a * 'a set -> 'a set" 445 :: MLSIG "val IN : ''a -> ''a set -> bool" 446 :: MLSIG "val UNION : ''a set -> ''a set -> ''a set" 447 :: MLSIG "val INTER : ''a set -> ''a set -> ''a set" 448 :: MLSIG "val DELETE : ''a set -> ''a -> ''a set" 449 :: MLSIG "val DIFF : ''a set -> ''a set -> ''a set" 450 :: MLSIG "val SUBSET : ''a set -> ''a set -> bool" 451 :: MLSIG "val PSUBSET : ''a set -> ''a set -> bool" 452 :: MLSIG "val IMAGE : ('a -> 'b) -> 'a set -> 'b set" 453 :: MLSIG "val BIGUNION : ''a set set -> ''a set" 454 :: MLSIG "val BIGINTER : ''a set set -> ''a set" 455 :: MLSIG "val CARD : ''a set -> num" 456 :: MLSIG "val DISJOINT : ''a set -> ''a set -> bool" 457 :: MLSIG "val CROSS : ''a set -> ''b set -> (''a * ''b) set" 458 :: MLSIG "val LIST_TO_SET : 'a list -> 'a set" 459 :: MLSIG "val IS_EMPTY : 'a set -> bool" 460 :: MLSIG "val SUM_IMAGE : (''a -> num) -> ''a set -> num" 461 :: MLSIG "val SUM_SET : num set -> num" 462 :: MLSIG "val MAX_SET : num set -> num" 463 :: MLSIG "val MIN_SET : num set -> num" 464 :: MLSIG "val count : num -> num set" 465 :: MLSIG "val POW : ''a set -> ''a set set" 466 :: defs 467 @ [MLSIG "val fromList : 'a list -> 'a set", 468 MLSIG "val toList : 'a set -> 'a list", 469 MLSTRUCT "fun fromList alist =\ 470 \ listML.FOLDL (fn s => fn a => INSERT(a,s)) EMPTY alist", 471 MLSTRUCT "fun toList EMPTY = []\n\ 472 \ | toList (INSERT(a,s)) = a::toList s"]) 473 474val _ = eCAML "set" 475 (MLSIGSTRUCT 476 ["type num = NumML.num", "", 477 "type 'a set = EMPTY | INSERT of 'a * 'a set"] @ 478 map MLSIG 479 ["val _IN : 'a -> 'a set -> bool", 480 "val _UNION : 'a set -> 'a set -> 'a set", 481 "val _INTER : 'a set -> 'a set -> 'a set", 482 "val _DELETE : 'a set -> 'a -> 'a set", 483 "val _DIFF : 'a set -> 'a set -> 'a set", 484 "val _SUBSET : 'a set -> 'a set -> bool", 485 "val _PSUBSET : 'a set -> 'a set -> bool", 486 "val _IMAGE : ('a -> 'b) -> 'a set -> 'b set", 487 "val _BIGUNION : 'a set set -> 'a set", 488 "val _BIGINTER : 'a set set -> 'a set", 489 "val _CARD : 'a set -> num", 490 "val _DISJOINT : 'a set -> 'a set -> bool", 491 "val _CROSS : 'a set -> 'b set -> ('a * 'b) set", 492 "val _SUM_IMAGE : ('a -> num) -> 'a set -> num", 493 "val _SUM_SET : num set -> num", 494 "val _MAX_SET : num set -> num", 495 "val _MIN_SET : num set -> num", 496 "val count : num -> num set", 497 "val _POW : 'a set -> 'a set set"] @ 498 defs) 499 500(* == Option ============================================================== *) 501 502val THE_NONE = Q.prove ( 503 `THE NONE = FAIL THE ^(mk_var("applied to NONE",bool)) NONE`, 504 REWRITE_TAC [combinTheory.FAIL_THM]); 505 506val _ = ConstMapML.insert_cons(Term.prim_mk_const{Name="SOME",Thy="option"}); 507val _ = ConstMapML.insert_cons(Term.prim_mk_const{Name="NONE",Thy="option"}); 508 509val defs = 510 map DEFN [OPTION_MAP_DEF, IS_SOME_DEF, IS_NONE_DEF, 511 CONJ THE_NONE THE_DEF, OPTION_JOIN_DEF]; 512 513val _ = eSML "option" 514 (MLSIGSTRUCT ["datatype option = datatype Option.option"] @ defs); 515 516val _ = eCAML "option" defs; 517 518val _ = adjoin_to_theory 519 {sig_ps = NONE, 520 struct_ps = SOME 521 (fn _ => 522 B [S "val _ = ConstMapML.insert_cons\ 523 \(Term.prim_mk_const{Name=\"SOME\",Thy=\"option\"});", NL, 524 S "val _ = ConstMapML.insert_cons\ 525 \(Term.prim_mk_const{Name=\"NONE\",Thy=\"option\"});", NL, NL])}; 526 527(* == Option ============================================================== *) 528 529val defs = 530 map DEFN [bool_size_def, pair_size_def, one_size_def, option_size_def]; 531 532val _ = eSML "basicSize" 533 (MLSIG "type num = numML.num" :: 534 MLSIG "type 'a option = 'a optionML.option" :: 535 MLSIG "type ('a,'b) sum = ('a,'b) sumML.sum" :: 536 OPEN ["num","sum","option"] :: 537 defs); 538 539val _ = eCAML "basicSize" (MLSIGSTRUCT ["type num = NumML.num"] @ defs); 540 541(* == List ================================================================ *) 542 543val LENGTH_THM = REWRITE_RULE [arithmeticTheory.ADD1] LENGTH; 544 545val HD_NIL = Q.prove(`HD [] = FAIL HD ^(mk_var("Empty list",bool)) []`, 546 REWRITE_TAC [combinTheory.FAIL_THM]); 547 548val TL_NIL = Q.prove(`TL [] = FAIL TL ^(mk_var("Empty list",bool)) []`, 549 REWRITE_TAC [combinTheory.FAIL_THM]); 550 551val MAP2_FAIL = Q.prove 552(`(!f h t. 553 (MAP2 (f:'a->'b->'c) [] (h::t) = 554 FAIL MAP2 ^(mk_var("unequal length lists",bool)) f [] (h::t))) /\ 555 !f h t. 556 (MAP2 (f:'a->'b->'c) (h::t) [] = 557 FAIL MAP2 ^(mk_var("unequal length lists",bool)) f (h::t) [])`, 558 REWRITE_TAC [combinTheory.FAIL_THM]); 559 560val MAP2_THM = let val [a,b] = CONJUNCTS MAP2 561 val [c,d] = CONJUNCTS MAP2_FAIL 562 in LIST_CONJ [a,c,d,b] 563 end; 564 565val ZIP_FAIL = Q.prove 566(`(!(h:'b) t. ZIP ([]:'a list,h::t) = 567 FAIL ZIP ^(mk_var("unequal length lists",bool)) ([],h::t)) /\ 568 (!(h:'a) t. ZIP (h::t,[]:'b list) = 569 FAIL ZIP ^(mk_var("unequal length lists",bool)) (h::t,[]))`, 570 REWRITE_TAC [combinTheory.FAIL_THM]); 571 572val ZIP_THM = let val [a,b] = CONJUNCTS ZIP 573 val [c,d] = CONJUNCTS ZIP_FAIL 574 in LIST_CONJ [a,c,d,b] 575 end; 576 577val LAST_NIL = Q.prove 578(`LAST [] = FAIL LAST ^(mk_var("empty list",bool)) []`, 579 REWRITE_TAC [combinTheory.FAIL_THM]); 580 581val FRONT_NIL = Q.prove 582(`FRONT [] = FAIL FRONT ^(mk_var("empty list",bool)) []`, 583 REWRITE_TAC [combinTheory.FAIL_THM]); 584 585val GENLIST_compute = Q.prove( 586 `!n l. 587 GENLIST f n = if n = 0 then [] else SNOC (f (PRE n)) (GENLIST f (PRE n))`, 588 STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC arithmeticTheory.num_CASES 589 THEN REWRITE_TAC [numTheory.NOT_SUC, prim_recTheory.PRE, GENLIST]); 590 591val defs = 592 map DEFN [NULL_DEF, CONJ HD_NIL HD, CONJ TL_NIL TL, APPEND, FLAT, MAP, 593 FILTER, FOLDR, FOLDL, SNOC, GENLIST_compute, EVERY_DEF, 594 EXISTS_DEF, MAP2_THM, ZIP_THM, UNZIP_THM, REVERSE_DEF, 595 CONJ LAST_NIL LAST_CONS, CONJ FRONT_NIL FRONT_CONS, 596 EL_compute, LENGTH_THM, LEN_DEF, REV_DEF, SUM, 597 list_size_def, PAD_LEFT, PAD_RIGHT] @ 598 [DEFN_NOSIG MEM, DEFN ALL_DISTINCT] 599 600val _ = eSML "list" 601 (MLSIG "type num = numML.num" :: 602 MLSIG "val MEM : ''a -> ''a list -> bool" :: 603 OPEN ["num"] :: 604 defs) 605 606val _ = eCAML "list" 607 (MLSIG "type num = NumML.num" :: 608 MLSIG "val _MEM : 'a -> 'a list -> bool" :: 609 MLSTRUCT "type num = NumML.num" :: 610 OPEN ["Num"] :: 611 defs) 612 613val _ = adjoin_to_theory 614 {sig_ps = NONE, 615 struct_ps = SOME (fn _ => 616 B [S "val _ = ConstMapML.insert\ 617 \ (Term.prim_mk_const{Name=\"CONS\",Thy=\"list\"});", NL, 618 S "val _ = ConstMapML.insert\ 619 \ (Term.prim_mk_const{Name=\"NIL\",Thy=\"list\"});", NL, NL])}; 620 621(* == Rich list =========================================================== *) 622 623val num_CASES = arithmeticTheory.num_CASES; 624 625val NOT_SUC = numTheory.NOT_SUC; 626val PRE = prim_recTheory.PRE; 627 628val BUTFIRSTN_compute = Q.prove( 629 `!n l. BUTFIRSTN n l = 630 if n = 0 then l else 631 if l = [] then 632 FAIL BUTFIRSTN ^(mk_var("List too short",bool)) n [] 633 else 634 BUTFIRSTN (PRE n) (TL l)`, 635 STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES 636 THEN1 REWRITE_TAC [BUTFIRSTN] 637 THEN STRIP_TAC THEN Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES 638 THEN REWRITE_TAC [NOT_CONS_NIL, TL, NOT_SUC, PRE, BUTFIRSTN, 639 combinTheory.FAIL_THM]); 640 641val ELL_compute = Q.prove( 642 `!n l. ELL n l = if n = 0 then LAST l else ELL (PRE n) (FRONT l)`, 643 STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES 644 THEN REWRITE_TAC [NOT_SUC, PRE, ELL]); 645 646val FIRSTN_compute = Q.prove( 647 `!n l. FIRSTN n l = 648 if n = 0 then [] else 649 if l = [] then 650 FAIL FIRSTN ^(mk_var("List too short",bool)) n [] 651 else 652 (HD l)::FIRSTN (PRE n) (TL l)`, 653 STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES 654 THEN1 REWRITE_TAC [FIRSTN] 655 THEN STRIP_TAC THEN Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES 656 THEN REWRITE_TAC [NOT_CONS_NIL, HD, TL, NOT_SUC, PRE, FIRSTN, 657 combinTheory.FAIL_THM]); 658 659val REPLICATE_compute = Q.prove( 660 `!n l. REPLICATE n l = if n = 0 then [] else l::(REPLICATE (PRE n) l)`, 661 STRIP_TAC THEN Q.SPEC_THEN `n` STRUCT_CASES_TAC num_CASES 662 THEN REWRITE_TAC [NOT_SUC, PRE, REPLICATE]); 663 664val SEG_compute = Q.prove( 665 `!m k l. SEG m k l = 666 if m = 0 then [] else 667 if l = [] then 668 FAIL SEG ^(mk_var("List too short",bool)) m k [] 669 else 670 if k = 0 then 671 (HD l)::SEG (PRE m) 0 (TL l) 672 else 673 SEG m (PRE k) (TL l)`, 674 STRIP_TAC THEN Q.SPEC_THEN `m` STRUCT_CASES_TAC num_CASES 675 THEN1 REWRITE_TAC [SEG] 676 THEN STRIP_TAC THEN Q.SPEC_THEN `k` STRUCT_CASES_TAC num_CASES 677 THEN STRIP_TAC THEN Q.SPEC_THEN `l` STRUCT_CASES_TAC list_CASES 678 THEN REWRITE_TAC [NOT_CONS_NIL, HD, TL, NOT_SUC, PRE, SEG, 679 combinTheory.FAIL_THM]); 680 681val LUPDATE_compute = Q.prove( 682`(!e n. LUPDATE e n [] = []) /\ 683 (!e n x l. LUPDATE e n (x::l) = 684 if n = 0 then e::l else x::LUPDATE e (PRE n) l)`, 685SRW_TAC[][LUPDATE_def] THEN 686Cases_on `n` THEN 687FULL_SIMP_TAC (srw_ss()) [LUPDATE_def]) 688 689val defs = 690 map DEFN [AND_EL_DEF,BUTFIRSTN_compute,ELL_compute,FIRSTN_compute, 691 BUTLASTN_compute,LASTN_compute, 692 IS_PREFIX,IS_SUBLIST,OR_EL_DEF,SPLITP_AUX_def, 693 LUPDATE_compute, REWRITE_RULE [FUN_EQ_THM] SPLITP_compute, 694 PREFIX_DEF,REPLICATE_compute, 695 SCANL,SCANR,SEG_compute,SUFFIX_DEF,UNZIP_FST_DEF,UNZIP_SND_DEF]; 696 697val _ = eSML "rich_list" 698 (MLSIG "type num = numML.num" 699 :: OPEN ["pair","num","list"] 700 :: defs) 701 702val _ = eCAML "rich_list" 703 (MLSIG "type num = NumML.num" 704 :: MLSTRUCT "type num = NumML.num" 705 :: OPEN ["pair","num","list"] 706 :: defs) 707 708(* == String ============================================================== *) 709 710val _ = app ConstMapML.insert [``$EXPLODE``, ``$IMPLODE``, ``$ORD``, ``$CHR``] 711 712val _ = ConstMapML.insert(prim_mk_const{Name="DEST_STRING",Thy="string"}); 713val _ = ConstMapML.insert(prim_mk_const{Name="string_lt",Thy="string"}); 714 715fun cpi (t,nm) = ConstMapML.prim_insert(t,(false,"",nm,type_of t)) 716 717val _ = cpi (``STRCAT``, "STRCAT") 718val _ = cpi (``STRLEN``, "STRLEN") 719val _ = cpi (``STRING``, "STRING") 720 721val PAD_LEFT = Q.prove( 722 `PAD_LEFT c n s = 723 STRCAT (IMPLODE (GENLIST (K c) (n - STRLEN s))) s`, 724 REWRITE_TAC [listTheory.PAD_LEFT, IMPLODE_EXPLODE_I]); 725 726val PAD_RIGHT = Q.prove( 727 `PAD_RIGHT c n s = 728 STRCAT s (IMPLODE (GENLIST (K c) (n - STRLEN s)))`, 729 REWRITE_TAC [listTheory.PAD_RIGHT, IMPLODE_EXPLODE_I]); 730 731val defs = 732 map DEFN [char_size_def, STRCAT_EXPLODE, 733 isPREFIX_DEF, isLower_def, isUpper_def, isDigit_def, isAlpha_def, 734 isHexDigit_def, isAlphaNum_def, isPrint_def, isSpace_def, 735 isGraph_def, isPunct_def, isAscii_def, isCntrl_def, 736 toLower_def, toUpper_def, PAD_LEFT, PAD_RIGHT, 737 char_lt_def, char_le_def, char_gt_def, char_ge_def, 738 string_le_def, string_gt_def, string_ge_def] 739 740val _ = eSML "string" 741 (OPEN ["num", "list", "option"] 742 :: MLSIG "type num = numML.num" 743 :: MLSIG "type char = Char.char" 744 :: MLSIG "type string = String.string" 745 :: MLSIG "val DEST_STRING : string -> (char * string) option" 746 :: MLSIG "val CHR : num -> char" 747 :: MLSIG "val ORD : char -> num" 748 :: MLSIG "val string_lt : string -> string -> bool" 749 :: MLSIG "val IMPLODE : char list -> string" 750 :: MLSIG "val EXPLODE : string -> char list" 751 :: MLSIG "val STRLEN : string -> num" 752 :: MLSTRUCT "type char = Char.char;" 753 :: MLSTRUCT "type string = String.string;" 754 :: MLSTRUCT "fun CHR n =\ 755 \ Char.chr(valOf(Int.fromString(numML.toDecString n)));" 756 :: MLSTRUCT "fun ORD c = numML.fromDecString(Int.toString(Char.ord c));" 757 :: MLSTRUCT "fun STRING c s = String.^(String.str c,s);" 758 :: MLSTRUCT "fun DEST_STRING s = if s = \"\" then NONE \n\ 759 \ else SOME(String.sub(s,0),String.extract(s,1,NONE));" 760 :: MLSTRUCT "fun string_lt a b = String.compare(a,b) = LESS" 761 :: MLSTRUCT "val IMPLODE = String.implode" 762 :: MLSTRUCT "val EXPLODE = String.explode" 763 :: MLSTRUCT "fun STRLEN s = LENGTH (EXPLODE s)" 764 :: defs) 765 766val _ = eCAML "string" 767 (MLSIGSTRUCT ["type num = NumML.num"] 768 @ OPEN ["list", "option"] 769 :: MLSIG "val _DEST_STRING : string -> (char * string) option" 770 :: MLSIG "val _CHR : num -> char" 771 :: MLSIG "val _ORD : char -> num" 772 :: MLSIG "val string_lt : string -> string -> bool" 773 :: MLSIG "val _IMPLODE : char list -> string" 774 :: MLSIG "val _EXPLODE : string -> char list" 775 :: MLSTRUCT "let _CHR n = Char.chr(NumML.int_of_holnum n)" 776 :: MLSTRUCT "let _ORD c = NumML.holnum_of_int(Char.code c)" 777 :: MLSTRUCT "let _STRING c s = String.concat \"\" [Char.escaped c; s]" 778 :: MLSTRUCT "let _DEST_STRING s = if s = \"\" then None\n\ 779 \ else Some(String.get s 0,String.sub s 1 (String.length s - 1))" 780 :: MLSTRUCT "let string_lt a b = String.compare a b < 0" 781 :: MLSTRUCT "let _IMPLODE l =\n\ 782 \ let s = String.create (List.length l) in\n\ 783 \ let _ = List.fold_left\n\ 784 \ (function n -> function c ->\ 785 \ (String.set s n c; n + 1)) 0 l in s" 786 :: MLSTRUCT "let _EXPLODE s =\n\ 787 \ Rich_listML._GENLIST\n\ 788 \ (function n -> String.get s (NumML.int_of_holnum n))\n\ 789 \ (NumML.holnum_of_int (String.length s))" 790 :: map DEFN [char_size_def, isLower_def, isUpper_def, isDigit_def, 791 isAlpha_def, isHexDigit_def, isAlphaNum_def, isPrint_def, isSpace_def, 792 isGraph_def, isPunct_def, isAscii_def, isCntrl_def, 793 toLower_def, toUpper_def, 794 char_lt_def, char_le_def, char_gt_def, char_ge_def, 795 string_le_def, string_gt_def, string_ge_def]) 796 797fun adjoin_to_theory_struct l = 798 adjoin_to_theory { 799 sig_ps = NONE, 800 struct_ps = SOME (fn _ => B (List.concat (map (fn s => [S s, NL]) l))) 801 }; 802 803val _ = adjoin_to_theory_struct [ 804 "val _ = app (fn n => ConstMapML.insert\ 805 \ (prim_mk_const{Name=n,Thy=\"string\"}))", 806 " [\"CHR\",\"ORD\",\"DEST_STRING\",\"string_lt\",\ 807 \ \"IMPLODE\",\"EXPLODE\"]"]; 808 809(* == Finite map ========================================================== *) 810 811val FAPPLY_FEMPTY = Q.prove 812(`FAPPLY (FEMPTY:('a,'b)fmap) x :'b = 813 FAIL FAPPLY ^(mk_var("empty map",bool)) FEMPTY x`, 814 REWRITE_TAC [combinTheory.FAIL_THM]); 815 816val DRESTRICT_PRED_THM = 817 SIMP_RULE std_ss [boolTheory.IN_DEF] 818 (CONJ DRESTRICT_FEMPTY DRESTRICT_FUPDATE); 819 820val DRESTRICT_PRED_THM = 821 SIMP_RULE std_ss [boolTheory.IN_DEF] 822 (CONJ DRESTRICT_FEMPTY DRESTRICT_FUPDATE); 823 824val th = GEN_ALL 825 (CONV_RULE (DEPTH_CONV ETA_CONV) 826 (ABS (Term `a:'a`) 827 (SIMP_RULE std_ss [IN_SING,IN_DEF] 828 (Q.SPEC `{x}` (Q.SPEC `a` IN_COMPL))))); 829 830val RRESTRICT_PRED_THM = Q.prove 831(`(!P. RRESTRICT (FEMPTY:'a|->'b) P = (FEMPTY:'a|->'b)) /\ 832 (!(f:'a|->'b) P x y. 833 RRESTRICT (f |+ (x,y)) P = 834 if P y then RRESTRICT f P |+ (x,y) 835 else RRESTRICT (DRESTRICT f (\a. ~(a = x))) P)`, 836 REWRITE_TAC [RRESTRICT_FEMPTY] 837 THEN METIS_TAC [REWRITE_RULE [th] RRESTRICT_FUPDATE, IN_DEF]); 838 839val FRANGE_EQNS = Q.prove 840(`(FRANGE (FEMPTY:'a|->'b) = ({}:'b -> bool)) /\ 841 (!(f:'a |-> 'b) (x:'a) (y:'b). 842 FRANGE (f |+ (x,y)) = y INSERT FRANGE (DRESTRICT f (\a. ~(a = x))))`, 843 METIS_TAC [REWRITE_RULE [th] FRANGE_FUPDATE, FRANGE_FEMPTY]); 844 845val o_f_EQNS = Q.prove 846(`(f o_f (FEMPTY:'a|->'b) = (FEMPTY:'a|->'c)) /\ 847 ((f:'b->'c) o_f ((fm:'a|->'b) |+ (k,v)) = (f o_f fm) |+ (k,f v))`, 848 METIS_TAC [o_f_FEMPTY, o_f_FUPDATE]) 849 850val T_INTRO = PURE_ONCE_REWRITE_RULE [PROVE[] (Term `x = (x = T)`)] 851 852val defs = 853 DEFN_NOSIG (CONJ FDOM_FEMPTY FDOM_FUPDATE) 854 :: map DEFN [CONJ FAPPLY_FEMPTY FAPPLY_FUPDATE_THM, 855 FCARD_DEF, FLOOKUP_DEF, REWRITE_RULE [FUN_EQ_THM] FUPDATE_LIST, 856 CONJ FUNION_FEMPTY_1 (CONJ FUNION_FEMPTY_2 FUNION_FUPDATE_1), 857 CONJ DOMSUB_FEMPTY DOMSUB_FUPDATE_THM, 858 CONJ (T_INTRO (SPEC_ALL SUBMAP_FEMPTY)) SUBMAP_FUPDATE, 859 DRESTRICT_PRED_THM, RRESTRICT_PRED_THM] 860 @ DEFN_NOSIG FRANGE_EQNS 861 :: map DEFN [o_f_EQNS, CONJ (T_INTRO (SPEC_ALL FEVERY_FEMPTY)) 862 (REWRITE_RULE [th] FEVERY_FUPDATE)] 863 864val _ = eSML "fmap" 865 (ABSDATATYPE (["'a","'b"], `fmap = FEMPTY | FUPDATE fmap ('a#'b)`) 866 :: OPEN ["num", "list", "set", "option"] 867 :: MLSIG "type num = numML.num" 868 :: MLSIG "type 'a set = 'a setML.set" 869 :: MLSIG "val FEMPTY : ('a,'b) fmap" 870 :: MLSIG "val FUPDATE : ('a,'b) fmap * ('a * 'b) -> ('a,'b)fmap" 871 :: MLSIG "val FDOM : ('a,'b) fmap -> 'a set" 872 :: defs) 873 874val _ = eCAML "fmap" 875 (MLSIGSTRUCT ["type num = NumML.num", "type 'a set = 'a SetML.set"] 876 @ ABSDATATYPE (["'a","'b"], `fmap = FEMPTY | FUPDATE fmap ('a # 'b)`) 877 :: OPEN ["num", "list", "set", "option"] 878 :: MLSIG "val _FDOM : ('a,'b) fmap -> 'a set" 879 :: MLSIG "val _FRANGE : ('a,'b) fmap -> 'b set" 880 :: defs) 881 882(* == Sum ================================================================= *) 883 884val OUTL_INR = Q.prove 885(`!y. OUTL(INR y:'a+'b) = 886 FAIL OUTL ^(mk_var("applied to INR",bool)) (INR y:'a+'b)`, 887 REWRITE_TAC [combinTheory.FAIL_THM]); 888 889val OUTR = Q.prove 890(`(!x. OUTR(INL x:'a+'b) = 891 FAIL OUTR ^(mk_var("applied to INL",bool)) (INL x:'a+'b)) /\ 892 (!y. OUTR(INR y:'a+'b) = y)`, 893 REWRITE_TAC [combinTheory.FAIL_THM,OUTR]); 894 895val ISL_THM = Q.prove 896(`(!x. ISL (INL x:'a+'b) = T) /\ !y. ISL (INR y:'a+'b) = F`, 897 REWRITE_TAC[ISL]); 898 899val ISR_THM = Q.prove 900(`(!x. ISR (INL x:'a+'b) = F) /\ !y. ISR (INR y:'a+'b) = T`, 901 REWRITE_TAC[ISR]) 902 903val defs = 904 DATATYPE `sum = INL 'a | INR 'b` 905 :: map DEFN [CONJ OUTL OUTL_INR, OUTR, ISL_THM, ISR_THM] 906 907val _ = eSML "sum" defs 908val _ = eCAML "sum" defs; 909 910(* == Bit ================================================================= *) 911 912val PRE = prim_recTheory.PRE; 913val NOT_SUC = numTheory.NOT_SUC; 914 915val NUMERAL_1 = Q.prove( 916 `!n. (NUMERAL (BIT1 n) = 1) = (n = 0)`, 917 REWRITE_TAC [GSYM (REWRITE_CONV [GSYM ALT_ZERO] ``NUMERAL (BIT1 0)``)] 918 THEN SIMP_TAC bool_ss [BIT1, NUMERAL_DEF] 919 THEN DECIDE_TAC); 920 921val NUMERAL_1b = Q.prove( 922 `!n. ~(NUMERAL (BIT2 n) = 1)`, 923 REWRITE_TAC [GSYM (REWRITE_CONV [GSYM ALT_ZERO] ``NUMERAL (BIT1 0)``)] 924 THEN SIMP_TAC bool_ss [BIT1, BIT2, NUMERAL_DEF] 925 THEN DECIDE_TAC); 926 927val iDUB_SUC = Q.prove(`!n. numeral$iDUB (SUC n) = BIT2 n`, 928 SIMP_TAC bool_ss [iDUB, BIT2, ADD1] THEN DECIDE_TAC); 929 930val DIV2_BIT1_SUC = Q.prove( 931 `!n. DIV2 (NUMERAL (BIT1 (SUC n))) = n + 1`, 932 REWRITE_TAC [DIV2_def] 933 THEN GEN_REWRITE_TAC (DEPTH_CONV o RATOR_CONV o RAND_CONV) empty_rewrites 934 [BIT1, Q.SPEC `BIT1 (SUC n)` NUMERAL_DEF] 935 THEN SIMP_TAC arith_ss [ADD1, ONCE_REWRITE_RULE [MULT_COMM] ADD_DIV_ADD_DIV]); 936 937val LOG2_compute = Q.prove( 938 `!n. LOG2 n = 939 if n = 0 then 940 FAIL LOG2 ^(mk_var("undefined",bool)) n 941 else 942 if n = 1 then 943 0 944 else 945 1 + LOG2 (DIV2 n)`, 946 Cases THEN REWRITE_TAC [NOT_SUC, combinTheory.FAIL_THM] 947 THEN Q.SPEC_TAC (`n'`,`n`) THEN CONV_TAC numLib.SUC_TO_NUMERAL_DEFN_CONV 948 THEN STRIP_TAC 949 THENL [ 950 REWRITE_TAC [NUMERAL_1] THEN Cases THEN RW_TAC arith_ss [numeral_log2] 951 THENL [PROVE_TAC [iDUB_removal, numeral_ilog2, ALT_ZERO], 952 REWRITE_TAC [iDUB_SUC, DIV2_BIT1_SUC, numeral_ilog2] 953 THEN SIMP_TAC arith_ss [iLOG2_def]], 954 REWRITE_TAC [NUMERAL_1b, numeral_div2, numeral_ilog2, numeral_log2, 955 NUMERAL_DEF, iLOG2_def, ADD1]]); 956 957val BITWISE_compute = Q.prove( 958 `!n opr a b. 959 BITWISE n opr a b = 960 if n = 0 then 0 else 961 2 * BITWISE (PRE n) opr (DIV2 a) (DIV2 b) + 962 (if opr (ODD a) (ODD b) then 1 else 0)`, 963 Cases THEN1 REWRITE_TAC [CONJUNCT1 BITWISE_def] 964 THEN REWRITE_TAC 965 [DIV2_def, NOT_SUC, PRE, EXP, BITWISE_EVAL, BIT0_ODD, SBIT_def]); 966 967val BIT_MODF_compute = Q.prove( 968 `!n f x b e y. 969 BIT_MODF n f x b e y = 970 if n = 0 then y else 971 BIT_MODF (PRE n) f (DIV2 x) (b + 1) (2 * e) 972 (if f b (ODD x) then e + y else y)`, 973 Cases THEN REWRITE_TAC [DIV2_def, NOT_SUC, PRE, BIT_MODF_def]); 974 975val BIT_REV_compute = Q.prove( 976 `!n x y. 977 BIT_REV n x y = 978 if n = 0 then y else 979 BIT_REV (PRE n) (DIV2 x) (2 * y + (if ODD x then 1 else 0))`, 980 Cases THEN REWRITE_TAC [DIV2_def, NOT_SUC, PRE, BIT_REV_def, EXP, SBIT_def]); 981 982val TIMES_2EXP_lem = Q.prove( 983 `!n. FUNPOW numeral$iDUB n 1 = 2 ** n`, 984 Induct THEN ASM_SIMP_TAC arith_ss 985 [EXP,CONJUNCT1 FUNPOW,FUNPOW_SUC,iDUB,GSYM TIMES2]); 986 987val TIMES_2EXP_compute = Q.prove( 988 `!n x. TIMES_2EXP n x = if x = 0 then 0 else x * FUNPOW numeral$iDUB n 1`, 989 RW_TAC bool_ss [MULT, TIMES_2EXP_lem, CONJUNCT1 FUNPOW, TIMES_2EXP_def]); 990 991val TIMES_2EXP1 = 992 (GSYM o REWRITE_RULE [arithmeticTheory.MULT_LEFT_1] o 993 Q.SPECL [`x`,`1`]) bitTheory.TIMES_2EXP_def; 994 995val MOD_2EXP_EQ_compute = Q.prove( 996 `!n a b. MOD_2EXP_EQ n a b = 997 if n = 0 then T else 998 (ODD a = ODD b) /\ MOD_2EXP_EQ (n - 1) (DIV2 a) (DIV2 b)`, 999 Cases THEN SRW_TAC [] [MOD_2EXP_EQ]) 1000 1001val BOOLIFY_compute = Q.prove( 1002 `!n. BOOLIFY n m a = 1003 if n = 0 then 1004 a 1005 else 1006 BOOLIFY (PRE n) (DIV2 m) (ODD m::a)`, 1007 Cases THEN SRW_TAC [] [BOOLIFY_def]); 1008 1009val HEX_compute = Q.prove( 1010 `!n. HEX n = 1011 if n = 0 then #"0" 1012 else if n = 1 then #"1" 1013 else if n = 2 then #"2" 1014 else if n = 3 then #"3" 1015 else if n = 4 then #"4" 1016 else if n = 5 then #"5" 1017 else if n = 6 then #"6" 1018 else if n = 7 then #"7" 1019 else if n = 8 then #"8" 1020 else if n = 9 then #"9" 1021 else if n = 10 then #"A" 1022 else if n = 11 then #"B" 1023 else if n = 12 then #"C" 1024 else if n = 13 then #"D" 1025 else if n = 14 then #"E" 1026 else if n = 15 then #"F" 1027 else FAIL HEX ^(mk_var("not a hex digit",bool)) n`, 1028 SRW_TAC [] [HEX_def,combinTheory.FAIL_THM]); 1029 1030val UNHEX_compute = Q.prove( 1031 `!n. UNHEX c = 1032 if c = #"0" then 0 1033 else if c = #"1" then 1 1034 else if c = #"2" then 2 1035 else if c = #"3" then 3 1036 else if c = #"4" then 4 1037 else if c = #"5" then 5 1038 else if c = #"6" then 6 1039 else if c = #"7" then 7 1040 else if c = #"8" then 8 1041 else if c = #"9" then 9 1042 else if c = #"A" then 10 1043 else if c = #"B" then 11 1044 else if c = #"C" then 12 1045 else if c = #"D" then 13 1046 else if c = #"E" then 14 1047 else if c = #"F" then 15 1048 else FAIL UNHEX ^(mk_var("not a hex digit",bool)) c`, 1049 SRW_TAC [] [UNHEX_def,combinTheory.FAIL_THM]) 1050 1051val LOWEST_SET_BIT_emit = Q.prove( 1052 `!n. LOWEST_SET_BIT n = 1053 if n = 0 then 1054 FAIL LOWEST_SET_BIT ^(mk_var("zero value",bool)) n 1055 else if ODD n then 1056 0 1057 else 1058 1 + LOWEST_SET_BIT (DIV2 n)`, 1059 SRW_TAC [] [LOWEST_SET_BIT, combinTheory.FAIL_THM]); 1060 1061val defs = 1062 map (DEFN o PURE_REWRITE_RULE [TIMES_2EXP1]) 1063 [TIMES_2EXP_compute,BITWISE_compute,LOG_compute,LOWEST_SET_BIT_emit, 1064 l2n_def,n2l_def,s2n_compute,n2s_compute,HEX_compute,UNHEX_compute, 1065 num_from_bin_list_def,num_from_oct_list_def,num_from_dec_list_def, 1066 num_from_hex_list_def,num_to_bin_list_def,num_to_oct_list_def, 1067 num_to_dec_list_def,num_to_hex_list_def,num_from_bin_string_def, 1068 num_from_oct_string_def,num_from_dec_string_def,num_from_hex_string_def, 1069 num_to_bin_string_def,num_to_oct_string_def,num_to_dec_string_def, 1070 num_to_hex_string_def, 1071 BIT_MODF_compute, BIT_MODIFY_EVAL, 1072 BIT_REV_compute, BIT_REVERSE_EVAL, 1073 LOG2_compute, DIVMOD_2EXP, SBIT_def, BITS_def, MOD_2EXP_EQ_compute, 1074 BITV_def, BIT_def, SLICE_def, SIGN_EXTEND_def, BOOLIFY_compute] 1075 1076val _ = eSML "bit" 1077 (MLSIG "type num = numML.num" :: 1078 OPEN ["num"] :: 1079 defs) 1080 1081val _ = eCAML "bit" 1082 (MLSIGSTRUCT ["type num = NumML.num"] @ 1083 OPEN ["num"] :: 1084 defs) 1085 1086(* == FCP ================================================================= *) 1087 1088val FCPi_def = Define `FCPi (f, (:'b)) = ($FCP f):'a ** 'b`; 1089 1090val mk_fcp_def = Define `mk_fcp = FCPi`; 1091 1092val index_comp = REWRITE_RULE [GSYM FCPi_def] index_comp; 1093val fcp_subst_comp = REWRITE_RULE [GSYM FCPi_def] fcp_subst_comp; 1094 1095val _ = new_constant("ITSELF", ``:num -> 'a itself``); 1096 1097val _ = new_constant("SUMi", ``:'a itself # 'b itself -> 'c itself``); 1098val _ = new_constant("MULi", ``:'a itself # 'b itself -> 'c itself``); 1099val _ = new_constant("EXPi", ``:'a itself # 'b itself -> 'c itself``); 1100 1101val SUMi = new_axiom("SUMi", ``SUMi (ITSELF a, ITSELF b) = ITSELF (a + b)``); 1102val MULi = new_axiom("MULi", ``MULi (ITSELF a, ITSELF b) = ITSELF (a * b)``); 1103val EXPi = new_axiom("EXPi", ``EXPi (ITSELF a, ITSELF b) = ITSELF (a ** b)``); 1104 1105val dimindexi = new_axiom("dimindexi", ``dimindex (ITSELF a) = a``); 1106 1107val _ = type_pp.pp_array_types := false 1108 1109val defs = [SUMi, MULi, EXPi, dimindexi, mk_fcp_def, index_comp, fcp_subst_comp] 1110 1111val _ = eSML "fcp" 1112 ([OPEN ["num"], 1113 MLSIG "type num = numML.num", 1114 DATATYPE(`itself = ITSELF num`), 1115 ABSDATATYPE (["'a","'b"], `cart = FCPi ((num -> 'a) # 'b itself)`), 1116 EQDATATYPE (["'a"],`bit0 = BIT0A 'a | BIT0B 'a`), 1117 EQDATATYPE (["'a"],`bit1 = BIT1A 'a | BIT1B 'a | BIT1C`)] @ 1118 map DEFN defs) 1119 1120val _ = eCAML "fcp" 1121 (MLSIGSTRUCT ["type num = NumML.num"] 1122 @ OPEN ["num"] 1123 :: DATATYPE(`itself = ITSELF num`) 1124 :: ABSDATATYPE (["'a","'b"], `cart = FCPi ((num -> 'a) # 'b itself)`) 1125 :: EQDATATYPE (["'a"],`bit0 = BIT0A 'a | BIT0B 'a`) 1126 :: EQDATATYPE (["'a"],`bit1 = BIT1A 'a | BIT1B 'a | BIT1C`) 1127 :: map (DEFN o REWRITE_RULE [GSYM FCPi_def, FUN_EQ_THM]) defs) 1128 1129(* == Words =============================================================== *) 1130 1131val word_index_def = Define `word_index (w:'a word) n = w ' n`; 1132val w2w_itself_def = Define `w2w_itself (:'a) w = (w2w w): 'a word`; 1133val sw2sw_itself_def = Define `sw2sw_itself (:'a) w = (sw2sw w): 'a word`; 1134val word_eq_def = Define `word_eq (v: 'a word) w = (v = w)`; 1135 1136val word_extract_itself_def = Define` 1137 word_extract_itself (:'a) h l w = (word_extract h l w): bool ** 'a`; 1138 1139val word_concat_itself_def = Define` 1140 word_concat_itself (:'a) v w = (word_concat v w): bool ** 'a`; 1141 1142val fromNum_def = Define` 1143 fromNum (n, (:'a)) = n2w_itself (n MOD dimword (:'a),(:'a))`; 1144 1145val _ = ConstMapML.insert_cons ``n2w_itself``; 1146 1147val sizes = [1, 2, 3, 4, 5, 6, 7, 8, 12, 16, 20, 24, 28, 30, 32, 64, 128, 256] 1148 1149val ALPHA_BETA_RULE = GEN_ALL o Q.INST [`a` |-> `m`, `b` |-> `n`] o SPEC_ALL 1150 1151val MOD_WL = 1152 (CONV_RULE (STRIP_QUANT_CONV (RHS_CONV (ONCE_REWRITE_CONV [GSYM n2w_mod])))) 1153 1154val TIMES_2EXP1 = 1155 (GSYM o REWRITE_RULE [arithmeticTheory.MULT_LEFT_1] o 1156 Q.SPECL [`x`,`1`]) bitTheory.TIMES_2EXP_def 1157 1158val word_reduce = Q.prove( 1159 `!b. $FCP (K b) = n2w (if b then 1 else 0) : 1 word`, 1160 SRW_TAC [fcpLib.FCP_ss] 1161 [word_index, DECIDE ``x < 1 = (x = 0n)``, fcpTheory.index_one, 1162 bitTheory.BITS_THM, bitTheory.BIT_def]); 1163 1164val bit_field_insert = Q.prove( 1165 `!h l a. 1166 bit_field_insert h l a w = 1167 word_modify 1168 (\i b. if l <= i /\ i <= h then word_index a (i - l) else b) w`, 1169 SRW_TAC [fcpLib.FCP_ss] 1170 [word_index_def, bit_field_insert_def, word_modify_def]); 1171 1172val n2w_w2n_RULE = REWRITE_RULE [n2w_w2n] o Q.SPEC `w2n w` 1173val word_eq_n2w = REWRITE_RULE [n2w_11] (Q.SPECL [`n2w m`,`n2w n`] word_eq_def) 1174val word_reduce_n2w = REWRITE_RULE [word_reduce] word_reduce_n2w 1175val word_eq_n2w = n2w_w2n_RULE (GEN_ALL word_eq_n2w) 1176val word_or_n2w = n2w_w2n_RULE word_or_n2w 1177val word_and_n2w = n2w_w2n_RULE word_and_n2w 1178val word_xor_n2w = n2w_w2n_RULE word_xor_n2w 1179val word_nor_n2w = n2w_w2n_RULE word_nor_n2w 1180val word_nand_n2w = n2w_w2n_RULE word_nand_n2w 1181val word_xnor_n2w = n2w_w2n_RULE word_xnor_n2w 1182val word_add_n2w = n2w_w2n_RULE word_add_n2w 1183val word_mul_n2w = n2w_w2n_RULE word_mul_n2w 1184val word_ge_n2w = n2w_w2n_RULE word_ge_n2w 1185val word_gt_n2w = n2w_w2n_RULE word_gt_n2w 1186val word_hi_n2w = n2w_w2n_RULE word_hi_n2w 1187val word_hs_n2w = n2w_w2n_RULE word_hs_n2w 1188val word_le_n2w = n2w_w2n_RULE word_le_n2w 1189val word_lo_n2w = n2w_w2n_RULE word_lo_n2w 1190val word_ls_n2w = n2w_w2n_RULE word_ls_n2w 1191val word_lt_n2w = n2w_w2n_RULE word_lt_n2w 1192val word_join_n2w = Q.SPECL [`n2w m`,`n2w n`] word_join_def 1193val word_div_n2w = Q.SPEC `n2w m` word_div_def 1194val word_asr_n2w = Q.SPECL [`n`,`n2w m`] word_asr_n2w 1195val word_lsr_n2w = Q.SPEC `n2w m` word_lsr_n2w 1196val word_rol_n2w = Q.SPEC `n2w m` word_rol_def 1197val reduce_and_n2w = Q.SPEC `n2w m` reduce_and 1198val reduce_or_n2w = Q.SPEC `n2w m` reduce_or 1199val sw2sw_n2w = Q.SPEC `n2w n` sw2sw_def 1200val add_with_carry_n2w = Q.SPEC `n2w n` add_with_carry_def 1201val word_sign_extend_n2w = 1202 REWRITE_RULE [w2n_n2w] (Q.SPECL [`n`,`n2w w`] word_sign_extend_def) 1203val reduce_xnor = 1204 ONCE_REWRITE_RULE [METIS_PROVE [] ``(<=>) = (\x y. x = y)``] reduce_xnor_def 1205 1206val f = 1207 map (DEFN o REWRITE_RULE 1208 [GSYM n2w_itself_def, GSYM w2w_itself_def, 1209 GSYM sw2sw_itself_def, GSYM word_concat_itself_def, 1210 GSYM word_extract_itself_def, word_T_def, word_L_def, word_H_def, 1211 TIMES_2EXP1, FUN_EQ_THM] o ALPHA_BETA_RULE) 1212 1213fun mk_index ocaml i = 1214 let val n = Arbnum.fromInt i 1215 val x = Int.toString i 1216 val typ = fcpLib.index_type n 1217 val s = String.extract(with_flag (type_pp.pp_num_types, false) 1218 type_to_string typ, 1, NONE) 1219 val w = "type word" ^ x ^ " = " ^ s ^ " word" 1220 val numML = if ocaml then "numML." else "NumML." 1221 val (a,b,c) = 1222 if ocaml then 1223 ("let toWord" ^ x ^ 1224 " n = fromNum (n,ITSELF(NumML.holnum_of_int " ^ x ^ "))", 1225 "val toWord" ^ x ^ " : NumML.num -> word" ^ x, 1226 "let fromString" ^ x ^ 1227 " = CombinML.o toWord" ^ x ^ " NumML.fromString") 1228 else 1229 ("fun toWord" ^ x ^ 1230 " n = fromNum (n,ITSELF(numML.fromInt " ^ x ^ "))", 1231 "val toWord" ^ x ^ " : numML.num -> word" ^ x, 1232 "val fromString" ^ x ^ 1233 " = o(toWord" ^ x ^ ", numML.fromString) : string -> word" ^ x) 1234 val d = "val fromString" ^ x ^ " : string -> word" ^ x 1235 in 1236 [EmitML.MLSTRUCT w, EmitML.MLSIG w, 1237 EmitML.MLSTRUCT a, EmitML.MLSIG b, 1238 EmitML.MLSTRUCT c, EmitML.MLSIG d] 1239 end; 1240 1241fun defs ocaml = 1242 f [dimword_def, fromNum_def] @ List.concat (map (mk_index ocaml) sizes) @ 1243 f [wordsTheory.INT_MIN_def, wordsTheory.UINT_MAX_def, 1244 wordsTheory.INT_MAX_def, 1245 w2n_n2w, word_eq_n2w, w2w_n2w, word_or_n2w, word_lsl_n2w, 1246 word_bits_n2w, word_signed_bits_n2w, Q.SPEC `c` word_bit_n2w, 1247 word_join_n2w, sw2sw_n2w, word_extract_n2w, word_slice_n2w, 1248 word_concat_def, word_log2_n2w, word_reverse_n2w, word_modify_n2w, 1249 word_lsb_n2w, word_msb_n2w, add_with_carry_n2w, 1250 word_1comp_n2w, word_and_n2w, word_xor_n2w, 1251 word_2comp_n2w, word_div_n2w, word_quot_def, 1252 MOD_WL word_add_n2w, word_sub_def, MOD_WL word_mul_n2w, 1253 word_lsr_n2w, word_asr_n2w, word_ror_n2w, word_rol_n2w, 1254 word_rrx_n2w, REWRITE_RULE [GSYM word_index_def] word_index_n2w, 1255 word_ge_n2w, word_gt_n2w, word_hi_n2w, word_hs_n2w, 1256 word_le_n2w, word_lo_n2w, word_ls_n2w, word_lt_n2w, 1257 word_reduce_n2w, reduce_and_n2w, reduce_or_n2w, reduce_xor_def, 1258 reduce_xnor, reduce_nand_def, reduce_nor_def, bit_field_insert, 1259 w2l_def,w2s_def, 1260 word_sign_extend_n2w, 1261 word_to_bin_list_def,word_to_oct_list_def, 1262 word_to_dec_list_def,word_to_hex_list_def, 1263 word_to_bin_string_def,word_to_oct_string_def, 1264 word_to_dec_string_def,word_to_hex_string_def] 1265 1266val _ = eSML "words" 1267 (OPEN ["sum", "num", "fcp", "bit"] 1268 :: MLSIG "type ('a, 'b) sum = ('a, 'b) sumML.sum" 1269 :: MLSIG "type 'a itself = 'a fcpML.itself" 1270 :: MLSIG "type 'a bit0 = 'a fcpML.bit0" 1271 :: MLSIG "type 'a bit1 = 'a fcpML.bit1" 1272 :: MLSIG "type num = numML.num" 1273 :: MLSIG "datatype 'a word = n2w_itself of num * 'a itself" 1274 :: MLSTRUCT "datatype 'a word = n2w_itself of num * 'a itself" 1275 :: defs false) 1276 1277val _ = eCAML "words" 1278 (MLSIGSTRUCT 1279 ["type num = NumML.num", 1280 "type ('a, 'b) sum = ('a, 'b) SumML.sum", 1281 "type 'a itself = 'a FcpML.itself", 1282 "type 'a bit0 = 'a FcpML.bit0", 1283 "type 'a bit1 = 'a FcpML.bit1", "", 1284 "type 'a word = N2w_itself of num * 'a itself"] @ 1285 OPEN ["sum", "num", "fcp", "bit"] :: 1286 defs true) 1287 1288fun WORDS_EMIT_RULE thm = 1289let 1290 val rws = List.map Conv.GSYM [word_index_def, n2w_itself_def, word_eq_def, 1291 w2w_itself_def, sw2sw_itself_def, word_concat_itself_def, 1292 word_extract_itself_def, literal_case_DEF] @ 1293 [BIT_UPDATE, fcp_n2w, word_T_def, word_L_def, word_H_def, 1294 literal_case_THM] 1295 val rule = Conv.CONV_RULE (Conv.STRIP_QUANT_CONV 1296 (Conv.RHS_CONV (Rewrite.PURE_REWRITE_CONV rws))) 1297 val thm = Rewrite.PURE_REWRITE_RULE [Conv.GSYM n2w_itself_def] thm 1298in 1299 Drule.LIST_CONJ (List.map (Conv.BETA_RULE o rule) (Drule.CONJUNCTS thm)) 1300end 1301 1302val _ = EmitML.reshape_thm_hook := (WORDS_EMIT_RULE o !EmitML.reshape_thm_hook) 1303 1304local 1305 val lines = [ 1306"val _ = ConstMapML.insert_cons", 1307" (Term.prim_mk_const{Name=\"n2w_itself\",Thy=\"words\"})", 1308"fun WORDS_EMIT_RULE thm = let", 1309" open boolTheory wordsTheory", 1310" val rws = List.map Conv.GSYM [word_index_def, n2w_itself_def, word_eq_def,", 1311" w2w_itself_def, sw2sw_itself_def, word_concat_itself_def,", 1312" word_extract_itself_def, literal_case_DEF] @", 1313" [BIT_UPDATE, fcp_n2w, word_T_def, word_L_def, word_H_def,", 1314" literal_case_THM]", 1315" val rule = Conv.CONV_RULE (Conv.STRIP_QUANT_CONV", 1316" (Conv.RHS_CONV (Rewrite.PURE_REWRITE_CONV rws)))", 1317" val thm = Rewrite.PURE_REWRITE_RULE [Conv.GSYM n2w_itself_def] thm", 1318"in", 1319" Drule.LIST_CONJ (List.map (Conv.BETA_RULE o rule) (Drule.CONJUNCTS thm))", 1320"end", 1321"val _ = EmitML.reshape_thm_hook :=\ 1322\ (WORDS_EMIT_RULE o !EmitML.reshape_thm_hook)"] 1323in 1324 val _ = adjoin_to_theory 1325 {sig_ps = SOME (fn _ => 1326 B [S "val WORDS_EMIT_RULE : thm -> thm", NL]), 1327 struct_ps = SOME (fn _ => 1328 B (List.concat (map (fn s => [S s, NL]) lines)))} 1329end 1330 1331(* == Integer ============================================================= *) 1332 1333val neg_int_of_num_def = Define `neg_int_of_num n = ~ int_of_num (n + 1)`; 1334val i2w_itself_def = Define `i2w_itself(i,(:'a)) = i2w i : 'a word`; 1335 1336val i2w_itself = REWRITE_RULE [i2w_def] i2w_itself_def; 1337 1338val emit_rule = SIMP_RULE std_ss [numeralTheory.iZ, NUMERAL_DEF]; 1339 1340fun emit_conv l1 l2 = LIST_CONJ 1341 (map (GEN_ALL o (SIMP_CONV (srw_ss()) (neg_int_of_num_def::l1) 1342 THENC REWRITE_CONV [GSYM neg_int_of_num_def])) l2); 1343 1344val lem1 = DECIDE ``~(n + 1n <= m) ==> (n + 1 - m = (n - m) + 1)``; 1345val lem2 = DECIDE ``m + 1n + (n + 1) = m + n + 1 + 1``; 1346 1347val INT_NEG_EMIT = Q.prove( 1348 `(!n. ~ (int_of_num n) = 1349 if n = 0 then int_of_num 0 else neg_int_of_num (n - 1)) /\ 1350 (!n. ~ (neg_int_of_num n) = int_of_num (n + 1))`, 1351 SRW_TAC [ARITH_ss] [neg_int_of_num_def]); 1352 1353val INT_ADD_EMIT = emit_conv [emit_rule INT_ADD_REDUCE, lem1, lem2] 1354 [``int_of_num m + int_of_num n``, 1355 ``neg_int_of_num m + int_of_num n``, 1356 ``int_of_num m + neg_int_of_num n``, 1357 ``neg_int_of_num m + neg_int_of_num n``]; 1358 1359val INT_SUB_EMIT = emit_conv [emit_rule INT_SUB_REDUCE] 1360 [``int_of_num m - int_of_num n``, 1361 ``neg_int_of_num m - int_of_num n``, 1362 ``int_of_num m - neg_int_of_num n``, 1363 ``neg_int_of_num m - neg_int_of_num n``]; 1364 1365val INT_MUL_EMIT = emit_conv [emit_rule INT_MUL_REDUCE] 1366 [``int_of_num m * int_of_num n``, 1367 ``neg_int_of_num m * int_of_num n``, 1368 ``int_of_num m * neg_int_of_num n``, 1369 ``neg_int_of_num m * neg_int_of_num n``]; 1370 1371val INT_LT_EMIT = emit_conv [emit_rule INT_LT_CALCULATE] 1372 [``int_of_num m < int_of_num n``, 1373 ``neg_int_of_num m < int_of_num n``, 1374 ``int_of_num m < neg_int_of_num n``, 1375 ``neg_int_of_num m < neg_int_of_num n``]; 1376 1377val INT_NEG_EXP = Q.prove( 1378 `!m n. 1379 neg_int_of_num m ** n = 1380 if EVEN n then 1381 int_of_num ((m + 1) ** n) 1382 else 1383 ~int_of_num ((m + 1) ** n)`, 1384 SRW_TAC [] [neg_int_of_num_def, INT_EXP_NEG] 1385 THEN FULL_SIMP_TAC std_ss [INT_EXP_NEG, GSYM ODD_EVEN]); 1386 1387val INT_EXP_EMIT = CONJ INT_EXP INT_NEG_EXP; 1388 1389val INT_Num_EMIT = Q.prove( 1390 `(!n. Num (int_of_num n) = n) /\ 1391 (!n. Num (neg_int_of_num n) = 1392 FAIL $Num ^(mk_var("negative",bool)) (neg_int_of_num n))`, 1393 SRW_TAC [] [combinTheory.FAIL_THM]); 1394 1395val INT_DIV_EMIT = Q.prove( 1396 `!i j. i / j = 1397 if j = 0 then FAIL $/ ^(mk_var("zero denominator",bool)) i j 1398 else 1399 ^((rhs o snd o dest_imp o snd o strip_forall o concl) int_div)`, 1400 SRW_TAC [] [combinTheory.FAIL_THM, int_div]); 1401 1402val INT_MOD_EMIT = Q.prove( 1403 `!i j. i % j = 1404 if j = 0 then FAIL $% ^(mk_var("zero denominator",bool)) i j 1405 else 1406 ^((rhs o snd o dest_imp o snd o strip_forall o concl) int_mod)`, 1407 SRW_TAC [] [combinTheory.FAIL_THM, int_mod]); 1408 1409val INT_QUOTE_EMIT = Q.prove( 1410 `!i j. i quot j = 1411 if j = 0 then FAIL $quot ^(mk_var("zero denominator",bool)) i j 1412 else 1413 ^((rhs o snd o dest_imp o snd o strip_forall o concl) int_quot)`, 1414 SRW_TAC [] [combinTheory.FAIL_THM, int_quot]); 1415 1416val INT_REM_EMIT = Q.prove( 1417 `!i j. i rem j = 1418 if j = 0 then FAIL $rem ^(mk_var("zero denominator",bool)) i j 1419 else 1420 ^((rhs o snd o dest_imp o snd o strip_forall o concl) int_rem)`, 1421 SRW_TAC [] [combinTheory.FAIL_THM, int_rem]); 1422 1423val _ = EmitML.is_int_literal_hook := intSyntax.is_int_literal; 1424val _ = EmitML.int_of_term_hook := intSyntax.int_of_term; 1425 1426val _ = temp_clear_overloads_on "&"; 1427val _ = temp_overload_on("int_of_num", ``integer$int_of_num``); 1428 1429val _ = eSML "int" 1430 (OPEN ["num", "words"] 1431 :: EQDATATYPE ([], `int = int_of_num num | neg_int_of_num num`) 1432 :: MLSIG "type num = numML.num" 1433 :: MLSIG "type 'a itself = 'a fcpML.itself" 1434 :: MLSIG "type 'a word = 'a wordsML.word" 1435 :: MLSIG "val int_of_num : num -> int" 1436 :: MLSIG "val fromInt : Int.int -> int" 1437 :: MLSIG "val toInt : int -> Int.int option" 1438 :: MLSIG "val fromString : string -> int" 1439 :: MLSTRUCT 1440 "fun fromString s =\n\ 1441 \ let val s = String.extract(s,0,SOME (Int.-(String.size s,1))) in\n\ 1442 \ if String.sub(s,0) = #\"-\" then\n\ 1443 \ let val s = String.extract(s,1,NONE) in\n\ 1444 \ neg_int_of_num (numML.PRE (numML.fromString s))\n\ 1445 \ end\n\ 1446 \ else\n\ 1447 \ int_of_num (numML.fromString s)\n\ 1448 \ end\n" 1449 :: MLSTRUCT 1450 "fun fromInt i =\n\ 1451 \ fromString (String.map (fn c => if c = #\"~\" then #\"-\" else c)\n\ 1452 \ (String.^(Int.toString i,\"i\")))\n" 1453 :: MLSTRUCT 1454 "fun toInt (int_of_num n) = numML.toInt n\n\ 1455 \ | toInt (neg_int_of_num n) =\n\ 1456 \ case numML.toInt n of\n\ 1457 \ SOME v => SOME (Int.-(Int.~ v,1))\n\ 1458 \ | NONE => NONE\n" 1459 :: map DEFN 1460 [INT_NEG_EMIT, INT_Num_EMIT, 1461 INT_LT_EMIT, INT_LE_CALCULATE, INT_GT_CALCULATE, INT_GE_CALCULATE, 1462 INT_ABS, INT_ADD_EMIT, INT_SUB_EMIT, INT_MUL_EMIT, INT_EXP_EMIT, 1463 INT_DIV_EMIT, INT_MOD_EMIT, INT_QUOTE_EMIT, INT_REM_EMIT, 1464 INT_MAX_def, INT_MIN_def, UINT_MAX_def, i2w_itself, w2i_def]) 1465 1466val _ = eCAML "int" 1467 (MLSIGSTRUCT 1468 ["type num = NumML.num", 1469 "type 'a itself = 'a FcpML.itself", 1470 "type 'a word = 'a WordsML.word"] 1471 @ EQDATATYPE ([], `int = int_of_num num | neg_int_of_num num`) 1472 :: MLSIG "val fromString : string -> int" 1473 :: MLSTRUCT 1474 "let fromString s =\n\ 1475 \ let s' = String.sub s 0 (String.length s - 1) in\n\ 1476 \ if String.get s' 0 = '-' then\n\ 1477 \ let s' = String.sub s' 1 (String.length s' - 1) in\n\ 1478 \ Neg_int_of_num (NumML._PRE (NumML.fromString s'))\n\ 1479 \ else\n\ 1480 \ Int_of_num (NumML.fromString s')\n" 1481 :: map DEFN 1482 [INT_NEG_EMIT, INT_Num_EMIT, 1483 INT_LT_EMIT, INT_LE_CALCULATE, INT_GT_CALCULATE, INT_GE_CALCULATE, 1484 INT_ABS, INT_ADD_EMIT, INT_SUB_EMIT, INT_MUL_EMIT, INT_EXP_EMIT, 1485 INT_DIV_EMIT, INT_MOD_EMIT, INT_QUOTE_EMIT, INT_REM_EMIT, 1486 INT_MAX_def, INT_MIN_def, UINT_MAX_def, i2w_itself, w2i_def]) 1487 1488(*---------------------------------------------------------------------------*) 1489(* Remind ML code generator about integer literals and how to take them apart*) 1490(*---------------------------------------------------------------------------*) 1491 1492val _ = 1493 adjoin_to_theory { 1494 sig_ps = NONE, 1495 struct_ps = SOME (fn _ => 1496 B [S "val _ = EmitML.is_int_literal_hook := intSyntax.is_int_literal;", 1497 NL, 1498 S "val _ = EmitML.int_of_term_hook := intSyntax.int_of_term;", NL, 1499 NL]) 1500 }; 1501 1502(* == Sorting ============================================================= *) 1503 1504val defs = 1505 OPEN ["list"] :: map DEFN [PART_DEF, PARTITION_DEF, QSORT_DEF, SORTED_DEF]; 1506 1507val _ = eSML "sorting" defs; 1508val _ = eCAML "sorting" defs; 1509 1510(* restore "standard" set type abbreviation to have pride of place *) 1511val _ = type_abbrev("set", alpha --> bool) 1512val _ = disable_tyabbrev_printing "set" 1513 1514val _ = export_theory (); 1515