1structure intReduce :> intReduce = 2struct 3 4open HolKernel boolLib integerTheory intSyntax simpLib 5 6val ERR = mk_HOL_ERR "intSimps"; 7 8(*---------------------------------------------------------------------------*) 9(* Integer-specific compset *) 10(*---------------------------------------------------------------------------*) 11 12val elim_thms = [INT_ADD_REDUCE, INT_SUB_REDUCE, INT_MUL_REDUCE, 13 INT_DIV_REDUCE, INT_MOD_REDUCE, INT_EXP_REDUCE, 14 INT_LT_REDUCE, INT_LE_REDUCE, INT_EQ_REDUCE, 15 INT_GT_REDUCE, INT_GE_REDUCE, INT_DIVIDES_REDUCE, 16 INT_ABS_NUM, INT_ABS_NEG, INT_QUOT_REDUCE, INT_REM_REDUCE, 17 INT_MAX, INT_MIN, NUM_OF_INT] 18 19fun add_int_compset cmp = computeLib.add_thms elim_thms cmp 20 21fun int_compset () = 22 let 23 val cmp = reduceLib.num_compset() 24 in 25 add_int_compset cmp; cmp 26 end 27 28(*---------------------------------------------------------------------------*) 29(* Reducer for ground integer expressions *) 30(*---------------------------------------------------------------------------*) 31 32val REDUCE_CONV = computeLib.CBV_CONV (int_compset()) 33 34(*---------------------------------------------------------------------------*) 35(* Add integer reductions to the global compset *) 36(*---------------------------------------------------------------------------*) 37 38val _ = let open computeLib in add_funs elim_thms end; 39 40(*---------------------------------------------------------------------------*) 41(* Ground reduction conversions for integers (suitable for inclusion in *) 42(* simplifier, or as stand-alone *) 43(*---------------------------------------------------------------------------*) 44 45local 46 val num_ty = numSyntax.num 47 val int_ty = intSyntax.int_ty 48 val x = mk_var("x",int_ty) 49 val y = mk_var("y",int_ty) 50 val n = mk_var("n",num_ty) 51 val basic_op_terms = 52 [plus_tm, minus_tm, mult_tm, div_tm, mod_tm, int_eq_tm, 53 less_tm, leq_tm, great_tm, geq_tm, divides_tm, rem_tm, quot_tm, 54 min_tm, max_tm] 55 val basic_op_patterns = map (fn t => list_mk_comb(t, [x,y])) basic_op_terms 56 val exp_pattern = list_mk_comb(exp_tm, [x,n]) 57 val abs_patterns = [lhs (#2 (strip_forall (concl INT_ABS_NEG))), 58 lhs (#2 (strip_forall (concl INT_ABS_NUM)))] 59 fun reducible t = is_int_literal t orelse numSyntax.is_numeral t 60 fun reducer t = 61 let val (_, args) = strip_comb t 62 in if List.all reducible args then REDUCE_CONV t else Conv.NO_CONV t 63 end 64 fun mk_conv pat = 65 {name = "Integer calculation", 66 key = SOME([], pat), trace = 2, 67 conv = K (K reducer)} 68 val rederr = ERR "RED_CONV" "Term not reducible" 69in 70val INT_REDUCE_ss = SSFRAG 71 {name=SOME"INT_REDUCE", 72 convs = map mk_conv (exp_pattern::(abs_patterns @ basic_op_patterns)), 73 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 74 75fun RED_CONV t = 76 let val (f, args) = strip_comb t 77 val _ = f = exp_tm orelse mem f basic_op_terms orelse raise rederr 78 val _ = List.all reducible args orelse raise rederr 79 val _ = not (Lib.can dom_rng (type_of t)) orelse raise rederr 80 in 81 REDUCE_CONV t 82 end 83 84end (* local *) ; 85 86(*---------------------------------------------------------------------------*) 87(* Add reducer to srw_ss *) 88(*---------------------------------------------------------------------------*) 89 90val _ = BasicProvers.augment_srw_ss [INT_REDUCE_ss]; 91 92(* Accumulate literal additions in integer expressions 93 (doesn't do coefficient gathering - just adds up literals, and 94 reassociates along the way) 95*) 96fun collect_additive_consts tm = let 97 val summands = strip_plus tm 98in 99 case summands of 100 [] => raise Fail "strip_plus returned [] in collect_additive_consts" 101 | [_] => NO_CONV tm 102 | _ => let 103 in 104 case partition is_int_literal summands of 105 ([], _) => NO_CONV tm 106 | ([_], _) => NO_CONV tm 107 | (_, []) => REDUCE_CONV tm 108 | (numerals, non_numerals) => let 109 val reorder_t = mk_eq(tm, 110 mk_plus(list_mk_plus non_numerals, 111 list_mk_plus numerals)) 112 val reorder_thm = 113 EQT_ELIM(AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM) reorder_t) 114 in 115 (K reorder_thm THENC REDUCE_CONV THENC 116 TRY_CONV (REWR_CONV INT_ADD_RID)) tm 117 end 118 end 119end 120 121end 122