src/ZF/int_arith.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 38715 6513ea67d95d
child 40312 dff9f73a3763
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 (*  Title:      ZF/int_arith.ML
     2     Author:     Larry Paulson
     3 
     4 Simprocs for linear arithmetic.
     5 *)
     6 
     7 structure Int_Numeral_Simprocs =
     8 struct
     9 
    10 (* abstract syntax operations *)
    11 
    12 fun mk_bit 0 = @{term "0"}
    13   | mk_bit 1 = @{term "succ(0)"}
    14   | mk_bit _ = sys_error "mk_bit";
    15 
    16 fun dest_bit @{term "0"} = 0
    17   | dest_bit @{term "succ(0)"} = 1
    18   | dest_bit _ = raise Match;
    19 
    20 fun mk_bin i =
    21   let
    22     fun term_of [] = @{term Pls}
    23       | term_of [~1] = @{term Min}
    24       | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
    25   in term_of (Numeral_Syntax.make_binary i) end;
    26 
    27 fun dest_bin tm =
    28   let
    29     fun bin_of @{term Pls} = []
    30       | bin_of @{term Min} = [~1]
    31       | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
    32       | bin_of _ = sys_error "dest_bin";
    33   in Numeral_Syntax.dest_binary (bin_of tm) end;
    34 
    35 
    36 (*Utilities*)
    37 
    38 fun mk_numeral i = @{const integ_of} $ mk_bin i;
    39 
    40 (*Decodes a binary INTEGER*)
    41 fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
    42      (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    43   | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    44 
    45 fun find_first_numeral past (t::terms) =
    46         ((dest_numeral t, rev past @ terms)
    47          handle TERM _ => find_first_numeral (t::past) terms)
    48   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    49 
    50 val zero = mk_numeral 0;
    51 val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
    52 
    53 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    54 fun mk_sum []        = zero
    55   | mk_sum [t,u]     = mk_plus (t, u)
    56   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    57 
    58 (*this version ALWAYS includes a trailing zero*)
    59 fun long_mk_sum []        = zero
    60   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    61 
    62 val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
    63 
    64 (*decompose additions AND subtractions as a sum*)
    65 fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
    66         dest_summing (pos, t, dest_summing (pos, u, ts))
    67   | dest_summing (pos, Const (@{const_name "zdiff"}, _) $ t $ u, ts) =
    68         dest_summing (pos, t, dest_summing (not pos, u, ts))
    69   | dest_summing (pos, t, ts) =
    70         if pos then t::ts else @{const zminus} $ t :: ts;
    71 
    72 fun dest_sum t = dest_summing (true, t, []);
    73 
    74 val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
    75 val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
    76 
    77 val one = mk_numeral 1;
    78 val mk_times = FOLogic.mk_binop @{const_name "zmult"};
    79 
    80 fun mk_prod [] = one
    81   | mk_prod [t] = t
    82   | mk_prod (t :: ts) = if t = one then mk_prod ts
    83                         else mk_times (t, mk_prod ts);
    84 
    85 val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
    86 
    87 fun dest_prod t =
    88       let val (t,u) = dest_times t
    89       in  dest_prod t @ dest_prod u  end
    90       handle TERM _ => [t];
    91 
    92 (*DON'T do the obvious simplifications; that would create special cases*)
    93 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
    94 
    95 (*Express t as a product of (possibly) a numeral with other sorted terms*)
    96 fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t
    97   | dest_coeff sign t =
    98     let val ts = sort Term_Ord.term_ord (dest_prod t)
    99         val (n, ts') = find_first_numeral [] ts
   100                           handle TERM _ => (1, ts)
   101     in (sign*n, mk_prod ts') end;
   102 
   103 (*Find first coefficient-term THAT MATCHES u*)
   104 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   105   | find_first_coeff past u (t::terms) =
   106         let val (n,u') = dest_coeff 1 t
   107         in  if u aconv u' then (n, rev past @ terms)
   108                           else find_first_coeff (t::past) u terms
   109         end
   110         handle TERM _ => find_first_coeff (t::past) u terms;
   111 
   112 
   113 (*Simplify #1*n and n*#1 to n*)
   114 val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
   115 
   116 val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
   117                @{thm zmult_minus1}, @{thm zmult_minus1_right}];
   118 
   119 val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
   120                 @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 
   121                @{thms bin.intros};
   122 val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
   123                @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
   124                @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
   125 
   126 (*To perform binary arithmetic*)
   127 val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
   128 
   129 (*To evaluate binary negations of coefficients*)
   130 val zminus_simps = @{thms NCons_simps} @
   131                    [@{thm integ_of_minus} RS @{thm sym},
   132                     @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
   133                     @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
   134 
   135 (*To let us treat subtraction as addition*)
   136 val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
   137 
   138 (*push the unary minus down*)
   139 val int_minus_mult_eq_1_to_2 = @{lemma "$- w $* z = w $* $- z" by simp};
   140 
   141 (*to extract again any uncancelled minuses*)
   142 val int_minus_from_mult_simps =
   143     [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
   144 
   145 (*combine unary minus with numeric literals, however nested within a product*)
   146 val int_mult_minus_simps =
   147     [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
   148 
   149 fun prep_simproc thy (name, pats, proc) =
   150   Simplifier.simproc_global thy name pats proc;
   151 
   152 structure CancelNumeralsCommon =
   153   struct
   154   val mk_sum            = (fn T:typ => mk_sum)
   155   val dest_sum          = dest_sum
   156   val mk_coeff          = mk_coeff
   157   val dest_coeff        = dest_coeff 1
   158   val find_first_coeff  = find_first_coeff []
   159   fun trans_tac _       = ArithData.gen_trans_tac @{thm iff_trans}
   160 
   161   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
   162   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   163   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   164   fun norm_tac ss =
   165     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   166     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   167     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   168 
   169   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   170   fun numeral_simp_tac ss =
   171     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   172     THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss)))
   173   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   174   end;
   175 
   176 
   177 structure EqCancelNumerals = CancelNumeralsFun
   178  (open CancelNumeralsCommon
   179   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   180   val mk_bal   = FOLogic.mk_eq
   181   val dest_bal = FOLogic.dest_eq
   182   val bal_add1 = @{thm eq_add_iff1} RS @{thm iff_trans}
   183   val bal_add2 = @{thm eq_add_iff2} RS @{thm iff_trans}
   184 );
   185 
   186 structure LessCancelNumerals = CancelNumeralsFun
   187  (open CancelNumeralsCommon
   188   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   189   val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
   190   val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
   191   val bal_add1 = @{thm less_add_iff1} RS @{thm iff_trans}
   192   val bal_add2 = @{thm less_add_iff2} RS @{thm iff_trans}
   193 );
   194 
   195 structure LeCancelNumerals = CancelNumeralsFun
   196  (open CancelNumeralsCommon
   197   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   198   val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
   199   val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
   200   val bal_add1 = @{thm le_add_iff1} RS @{thm iff_trans}
   201   val bal_add2 = @{thm le_add_iff2} RS @{thm iff_trans}
   202 );
   203 
   204 val cancel_numerals =
   205   map (prep_simproc @{theory})
   206    [("inteq_cancel_numerals",
   207      ["l $+ m = n", "l = m $+ n",
   208       "l $- m = n", "l = m $- n",
   209       "l $* m = n", "l = m $* n"],
   210      K EqCancelNumerals.proc),
   211     ("intless_cancel_numerals",
   212      ["l $+ m $< n", "l $< m $+ n",
   213       "l $- m $< n", "l $< m $- n",
   214       "l $* m $< n", "l $< m $* n"],
   215      K LessCancelNumerals.proc),
   216     ("intle_cancel_numerals",
   217      ["l $+ m $<= n", "l $<= m $+ n",
   218       "l $- m $<= n", "l $<= m $- n",
   219       "l $* m $<= n", "l $<= m $* n"],
   220      K LeCancelNumerals.proc)];
   221 
   222 
   223 (*version without the hyps argument*)
   224 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
   225 
   226 structure CombineNumeralsData =
   227   struct
   228   type coeff            = int
   229   val iszero            = (fn x => x = 0)
   230   val add               = op + 
   231   val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   232   val dest_sum          = dest_sum
   233   val mk_coeff          = mk_coeff
   234   val dest_coeff        = dest_coeff 1
   235   val left_distrib      = @{thm left_zadd_zmult_distrib} RS @{thm trans}
   236   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   237   fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
   238 
   239   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
   240   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   241   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   242   fun norm_tac ss =
   243     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   244     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   245     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   246 
   247   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   248   fun numeral_simp_tac ss =
   249     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   250   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   251   end;
   252 
   253 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   254 
   255 val combine_numerals =
   256   prep_simproc @{theory}
   257     ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
   258 
   259 
   260 
   261 (** Constant folding for integer multiplication **)
   262 
   263 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   264   the "sum" of #3, x, #4; the literals are then multiplied*)
   265 
   266 
   267 structure CombineNumeralsProdData =
   268   struct
   269   type coeff            = int
   270   val iszero            = (fn x => x = 0)
   271   val add               = op *
   272   val mk_sum            = (fn T:typ => mk_prod)
   273   val dest_sum          = dest_prod
   274   fun mk_coeff(k,t) = if t=one then mk_numeral k
   275                       else raise TERM("mk_coeff", [])
   276   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   277   val left_distrib      = @{thm zmult_assoc} RS @{thm sym} RS @{thm trans}
   278   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   279   fun trans_tac _       = ArithData.gen_trans_tac @{thm trans}
   280 
   281 
   282 
   283 val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   284   val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS @{thm sym}] @
   285     bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
   286   fun norm_tac ss =
   287     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   288     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   289 
   290   val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
   291   fun numeral_simp_tac ss =
   292     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   293   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
   294   end;
   295 
   296 
   297 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   298 
   299 val combine_numerals_prod =
   300   prep_simproc @{theory}
   301     ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
   302 
   303 end;
   304 
   305 
   306 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   307 Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
   308              Int_Numeral_Simprocs.combine_numerals_prod];
   309 
   310 
   311 (*examples:*)
   312 (*
   313 print_depth 22;
   314 set timing;
   315 set trace_simp;
   316 fun test s = (Goal s; by (Asm_simp_tac 1));
   317 val sg = #sign (rep_thm (topthm()));
   318 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
   319 val (t,_) = FOLogic.dest_eq t;
   320 
   321 (*combine_numerals_prod (products of separate literals) *)
   322 test "#5 $* x $* #3 = y";
   323 
   324 test "y2 $+ ?x42 = y $+ y2";
   325 
   326 test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
   327 
   328 test "#9$*x $+ y = x$*#23 $+ z";
   329 test "y $+ x = x $+ z";
   330 
   331 test "x : int ==> x $+ y $+ z = x $+ z";
   332 test "x : int ==> y $+ (z $+ x) = z $+ x";
   333 test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
   334 test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
   335 
   336 test "#-3 $* x $+ y $<= x $* #2 $+ z";
   337 test "y $+ x $<= x $+ z";
   338 test "x $+ y $+ z $<= x $+ z";
   339 
   340 test "y $+ (z $+ x) $< z $+ x";
   341 test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
   342 test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
   343 
   344 test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
   345 test "u : int ==> #2 $* u = u";
   346 test "(i $+ j $+ #12 $+ k) $- #15 = y";
   347 test "(i $+ j $+ #12 $+ k) $- #5 = y";
   348 
   349 test "y $- b $< b";
   350 test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
   351 
   352 test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
   353 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
   354 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
   355 test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
   356 
   357 test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
   358 test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
   359 
   360 test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
   361 
   362 test "a $+ $-(b$+c) $+ b = d";
   363 test "a $+ $-(b$+c) $- b = d";
   364 
   365 (*negative numerals*)
   366 test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
   367 test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
   368 test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
   369 test "(i $+ j $+ #-12 $+ k) $- #15 = y";
   370 test "(i $+ j $+ #12 $+ k) $- #-15 = y";
   371 test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
   372 
   373 (*Multiplying separated numerals*)
   374 Goal "#6 $* ($# x $* #2) =  uu";
   375 Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
   376 *)
   377