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